---

Step * of Lemma Euclid-Prop19

∀e:EuclideanPlane. ∀a,b,c:Point.  (a # bc ⇒ bca < abc ⇒ |ab| < |ac|)
BY
{ (Auto
   THEN (Assert ∃d:Point. b=d=c BY
               (((InstLemma `Euclid-midpoint` [⌜e⌝;⌜b⌝;⌜c⌝]⋅ THEN Auto) THEN ExRepD) THEN D 0 With ⌜d⌝  THEN Auto))
   THEN (ExRepD
         THEN (Assert d # ba BY
                     (((FLemma `midpoint-sep` [-1] THENA Auto) THEN D -2)
                      THEN InstLemma `colinear-lsep` [⌜e⌝;⌜c⌝;⌜b⌝;⌜a⌝;⌜d⌝]⋅
                      THEN Auto))
         )
   THEN (Assert ∃E:Point. (a=d=E ∧ bE ≅ ca) BY
               ((((gProperProlong ⌜a⌝⌜d⌝`E'⌜a⌝⌜d⌝⋅ THEN Auto) THEN ExRepD) THEN D 0 With ⌜E⌝  THEN EAuto 1)
                THEN InstLemma `geo-midpoint-diagonals-congruent` [⌜e⌝;⌜d⌝;⌜b⌝;⌜E⌝;⌜c⌝;⌜a⌝]⋅
                THEN EAuto 1))) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. bca < abc
7. d : Point
8. b=d=c
9. d # ba
10. ∃E:Point. (a=d=E ∧ bE ≅ ca)
⊢ |ab| < |ac|

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c:Point.    (a  \#  bc  {}\mRightarrow{}  bca  <  abc  {}\mRightarrow{}  |ab|  <  |ac|)


By

---

Latex:
(Auto
  THEN  (Assert  \mexists{}d:Point.  b=d=c  BY
                          (((InstLemma  `Euclid-midpoint`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  ExRepD)
                            THEN  D  0  With  \mkleeneopen{}d\mkleeneclose{} 
                            THEN  Auto))
  THEN  (ExRepD
              THEN  (Assert  d  \#  ba  BY
                                      (((FLemma  `midpoint-sep`  [-1]  THENA  Auto)  THEN  D  -2)
                                        THEN  InstLemma  `colinear-lsep`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}
                                        THEN  Auto))
              )
  THEN  (Assert  \mexists{}E:Point.  (a=d=E  \mwedge{}  bE  \mcong{}  ca)  BY
                          ((((gProperProlong  \mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}d\mkleeneclose{}`E'\mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}d\mkleeneclose{}\mcdot{}  THEN  Auto)  THEN  ExRepD)
                              THEN  D  0  With  \mkleeneopen{}E\mkleeneclose{} 
                              THEN  EAuto  1)
                            THEN  InstLemma  `geo-midpoint-diagonals-congruent`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}E\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}
                            THEN  EAuto  1)))

---

Home Index