---

Step * 1 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)
20. ab ≅ e1f
21. bad ≅a fe1d
⊢ |ab| < |ac|
BY
{ (ExRepD
   THEN (Assert gad ≅a fe1d BY
               (((Assert cad ≅a gad BY
                        (InstLemma `out-cong-angle` [⌜e⌝;⌜c⌝;⌜a⌝;⌜d⌝;⌜g⌝;⌜d⌝]⋅ THEN EAuto 1))
                 THEN InstLemma `geo-between-out` [⌜e⌝;⌜a⌝;⌜g⌝;⌜c⌝]⋅
                 THEN EAuto 1)
                THEN (InstLemma `geo-cong-angle-transitivity` [⌜e⌝;⌜g⌝;⌜a⌝;⌜d⌝;⌜c⌝;⌜a⌝;⌜d⌝;⌜b⌝;⌜a⌝;⌜d⌝]⋅ THEN EAuto 1)
                THEN InstLemma `geo-cong-angle-transitivity` [⌜e⌝;⌜g⌝;⌜a⌝;⌜d⌝;⌜b⌝;⌜a⌝;⌜d⌝;⌜f⌝;⌜e1⌝;⌜d⌝]⋅
                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
15. b-d-f
16. d-f-c
17. df ≅ bd
18. f # e1d
19. g : Point
20. e1-f-g
21. a-g-c
22. ab ≅ e1f
23. bad ≅a fe1d
24. gad ≅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)
20.  ab  \mcong{}  e1f
21.  bad  \mcong{}\msuba{}  fe1d
\mvdash{}  |ab|  <  |ac|


By

---

Latex:
(ExRepD
  THEN  (Assert  gad  \mcong{}\msuba{}  fe1d  BY
                          (((Assert  cad  \mcong{}\msuba{}  gad  BY
                                            (InstLemma  `out-cong-angle`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THEN  EAuto  1))
                              THEN  InstLemma  `geo-between-out`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}
                              THEN  EAuto  1)
                            THEN  (InstLemma  `geo-cong-angle-transitivity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}
                                        ]\mcdot{}
                                        THEN  EAuto  1
                                        )
                            THEN  InstLemma  `geo-cong-angle-transitivity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}
                            ]\mcdot{}
                            THEN  EAuto  1))
  )

---

Home Index