---

Step * 1 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
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|
BY
{ ((Assert ab ≅ e1f BY
          ((InstLemma `geo-midpoint-diagonals-congruent` [⌜e⌝;⌜d⌝;⌜e1⌝;⌜f⌝;⌜a⌝;⌜b⌝]⋅ THEN Auto) THEN D 0 THEN Auto))
   THEN (Assert bad ≅a fe1d BY
               ((Assert bda ≅a fde1 BY
                       ((InstLemma `vert-angles-congruent` [⌜e⌝;⌜d⌝;⌜b⌝;⌜f⌝;⌜a⌝;⌜e1⌝]⋅
                         THENA (Auto THEN Unfold `geo-triangle` 0 THEN EAuto 1)
                         )
                        THEN Auto
                        ))
                THEN (InstLemma `Euclid-Prop4` [⌜e⌝;⌜d⌝;⌜b⌝;⌜a⌝;⌜d⌝;⌜f⌝;⌜e1⌝]⋅ THEN Auto)
                THEN Unfold `geo-tri` 0
                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)
20. ab ≅ e1f
21. bad ≅a fe1d
⊢ |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.  f  :  Point
15.  b-d-f
16.  d-f-c
17.  df  \mcong{}  bd
18.  f  \#  e1d
19.  \mexists{}g:Point.  (e1-f-g  \mwedge{}  a-g-c)
\mvdash{}  |ab|  <  |ac|


By

---

Latex:
((Assert  ab  \mcong{}  e1f  BY
                ((InstLemma  `geo-midpoint-diagonals-congruent`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THEN  Auto)
                  THEN  D  0
                  THEN  Auto))
  THEN  (Assert  bad  \mcong{}\msuba{}  fe1d  BY
                          ((Assert  bda  \mcong{}\msuba{}  fde1  BY
                                          ((InstLemma  `vert-angles-congruent`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{}]\mcdot{}
                                              THENA  (Auto  THEN  Unfold  `geo-triangle`  0  THEN  EAuto  1)
                                              )
                                            THEN  Auto
                                            ))
                            THEN  (InstLemma  `Euclid-Prop4`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{}]\mcdot{}  THEN  Auto)
                            THEN  Unfold  `geo-tri`  0
                            THEN  Auto))
  )

---

Home Index