---

Step * 1 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
26. |ab| < |e1g|
⊢ |ab| < |ac|
BY
{ ((Assert |ag| < |ac| BY
          (Unfold `geo-lt` 0
           THEN (InstConcl  [⌜g⌝;⌜c⌝]⋅ THEN Auto)
           THEN D -7
           THEN FLemma `geo-add-length-between` [-8]
           THEN EAuto 1))
   THEN ((Assert |e1g| = |ag| ∈ Length BY
                Auto)
         THEN InstLemma `geo-lt_transitivity` [⌜e⌝;⌜|ab|⌝;⌜|ag|⌝;⌜|ac|⌝]⋅
         THEN Auto)
   THEN FLemma `geo-le_weakening-lt` [-3]
   THEN Auto) }

---

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
26.  |ab|  <  |e1g|
\mvdash{}  |ab|  <  |ac|


By

---

Latex:
((Assert  |ag|  <  |ac|  BY
                (Unfold  `geo-lt`  0
                  THEN  (InstConcl    [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THEN  Auto)
                  THEN  D  -7
                  THEN  FLemma  `geo-add-length-between`  [-8]
                  THEN  EAuto  1))
  THEN  ((Assert  |e1g|  =  |ag|  BY
                            Auto)
              THEN  InstLemma  `geo-lt\_transitivity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}|ab|\mkleeneclose{};\mkleeneopen{}|ag|\mkleeneclose{};\mkleeneopen{}|ac|\mkleeneclose{}]\mcdot{}
              THEN  Auto)
  THEN  FLemma  `geo-le\_weakening-lt`  [-3]
  THEN  Auto)

---

Home Index