---

Step * 1 1 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
20. e1-f-g
21. a-g-c
22. ab ≅ e1f
23. bad ≅a fe1d
24. gad ≅a fe1d
25. ag ≅ e1g
⊢ |ab| < |ac|
BY
{ (Assert |ab| < |e1g| BY
         (((Assert |e1f| = |ab| ∈ Length BY
                  Auto)
           THEN (Assert |e1f| < |e1g| BY
                       (Unfold `geo-lt` 0
                        THEN (InstConcl  [⌜f⌝;⌜g⌝]⋅ THEN Auto)
                        THEN D -8
                        THEN FLemma `geo-add-length-between` [-9]
                        THEN EAuto 1))
           )
          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
20. e1-f-g
21. a-g-c
22. ab ≅ e1f
23. bad ≅a fe1d
24. gad ≅a fe1d
25. ag ≅ e1g
26. |ab| < |e1g|
⊢ |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.  g  :  Point
20.  e1-f-g
21.  a-g-c
22.  ab  \mcong{}  e1f
23.  bad  \mcong{}\msuba{}  fe1d
24.  gad  \mcong{}\msuba{}  fe1d
25.  ag  \mcong{}  e1g
\mvdash{}  |ab|  <  |ac|


By

---

Latex:
(Assert  |ab|  <  |e1g|  BY
              (((Assert  |e1f|  =  |ab|  BY
                                Auto)
                  THEN  (Assert  |e1f|  <  |e1g|  BY
                                          (Unfold  `geo-lt`  0
                                            THEN  (InstConcl    [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{}]\mcdot{}  THEN  Auto)
                                            THEN  D  -8
                                            THEN  FLemma  `geo-add-length-between`  [-9]
                                            THEN  EAuto  1))
                  )
                THEN  Auto
                ))

---

Home Index