---

Step * 1 of Lemma Euclid-Prop19-lemma1


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|
BY
{ ((ExRepD THEN (Assert f # e1d BY ((Assert a # df BY EAuto 1) THEN (Assert a # e1f BY EAuto 1) THEN Auto)))
   THEN (Assert ∃g:Point. (e1-f-g ∧ a-g-c) BY
               (((InstLemma `outer-pasch-strict` [⌜e⌝;⌜e1⌝;⌜d⌝;⌜a⌝;⌜f⌝;⌜c⌝]⋅ THENA Auto) THEN ExRepD)
                THEN D 0 With ⌜p⌝ 
                THEN Auto))
   ) }

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
15. b-d-f
16. d-f-c
17. df ≅ bd
18. f # e1d
19. ∃g:Point. (e1-f-g ∧ a-g-c)
⊢ |ab| < |ac|

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  a  \#  bc
7.  bad  \mcong{}\msuba{}  cad
8.  b-d-c
9.  |bd|  <  |cd|
10.  a  \#  bd
11.  e1  :  Point
12.  a-d-e1
13.  de1  \mcong{}  ad
14.  \mexists{}f:Point.  ((b-d-f  \mwedge{}  d-f-c)  \mwedge{}  df  \mcong{}  bd)
\mvdash{}  |ab|  <  |ac|


By

---

Latex:
((ExRepD
    THEN  (Assert  f  \#  e1d  BY
                            ((Assert  a  \#  df  BY  EAuto  1)  THEN  (Assert  a  \#  e1f  BY  EAuto  1)  THEN  Auto))
    )
  THEN  (Assert  \mexists{}g:Point.  (e1-f-g  \mwedge{}  a-g-c)  BY
                          (((InstLemma  `outer-pasch-strict`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  ExRepD)
                            THEN  D  0  With  \mkleeneopen{}p\mkleeneclose{} 
                            THEN  Auto))
  )

---

Home Index