---

Step * of Lemma Euclid-Prop19-lemma1

∀e:EuclideanPlane. ∀a,b,c,d:Point.  (a # bc ⇒ bad ≅a cad ⇒ b-d-c ⇒ |bd| < |cd| ⇒ |ab| < |ac|)
BY
{ ((Auto
    THEN (Assert a # bd BY
                (InstLemma `colinear-lsep` [⌜e⌝;⌜c⌝;⌜b⌝;⌜a⌝;⌜d⌝]⋅ THEN Auto))
    THEN gProperProlong ⌜a⌝⌜d⌝`e1'⌜a⌝⌜d⌝⋅
    THEN Auto)
   THEN (Assert ∃f:Point. ((b-d-f ∧ d-f-c) ∧ df ≅ bd) BY
               (((gProperProlong ⌜b⌝⌜d⌝`f'⌜b⌝⌜d⌝⋅ THEN Auto) THEN ExRepD)
                THEN (D 0 With ⌜f⌝  THEN Auto)
                THEN ((Assert |bd| = |df| ∈ Length BY EAuto 1) THEN (RWO "-1" 9 THENA Auto))
                THEN (InstLemma `geo-lt-out-to-between` [⌜e⌝;⌜d⌝;⌜f⌝;⌜c⌝]⋅ THEN Auto)
                THEN InstLemma `geo-out-iff-between1` [⌜e⌝;⌜d⌝;⌜f⌝;⌜c⌝;⌜b⌝]⋅
                THEN EAuto 1))
   ) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a # bc
7. bad ≅a cad
8. b-d-c
9. |bd| < |cd|
10. a # bd
11. e1 : Point
12. a-d-e1
13. de1 ≅ ad
14. ∃f:Point. ((b-d-f ∧ d-f-c) ∧ df ≅ bd)
⊢ |ab| < |ac|

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,d:Point.    (a  \#  bc  {}\mRightarrow{}  bad  \mcong{}\msuba{}  cad  {}\mRightarrow{}  b-d-c  {}\mRightarrow{}  |bd|  <  |cd|  {}\mRightarrow{}  |ab|  <  |ac|)


By

---

Latex:
((Auto
    THEN  (Assert  a  \#  bd  BY
                            (InstLemma  `colinear-lsep`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THEN  Auto))
    THEN  gProperProlong  \mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}d\mkleeneclose{}`e1'\mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}d\mkleeneclose{}\mcdot{}
    THEN  Auto)
  THEN  (Assert  \mexists{}f:Point.  ((b-d-f  \mwedge{}  d-f-c)  \mwedge{}  df  \mcong{}  bd)  BY
                          (((gProperProlong  \mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}d\mkleeneclose{}`f'\mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}d\mkleeneclose{}\mcdot{}  THEN  Auto)  THEN  ExRepD)
                            THEN  (D  0  With  \mkleeneopen{}f\mkleeneclose{}    THEN  Auto)
                            THEN  ((Assert  |bd|  =  |df|  BY  EAuto  1)  THEN  (RWO  "-1"  9  THENA  Auto))
                            THEN  (InstLemma  `geo-lt-out-to-between`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THEN  Auto)
                            THEN  InstLemma  `geo-out-iff-between1`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}
                            THEN  EAuto  1))
  )

---

Home Index