---

Step * 1 1 of Lemma Euclid-Prop19


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. bca < abc
7. d : Point
8. b=d=c
9. d # ba
10. E : Point
11. a=d=E
12. bE ≅ ca
13. dbE < abd
⊢ |ab| < |ac|
BY
{ (Assert ∃f:Point. ((abf ≅a Ebf ∧ a-f-E) ∧ |af| < |Ef|) BY
         ((InstLemma `Euclid-Prop9-with-between` [⌜e⌝;⌜a⌝;⌜E⌝;⌜b⌝]⋅ THEN Auto)
          THEN ExRepD
          THEN (InstLemma `Euclid-Prop19-lemma2` [⌜e⌝;⌜a⌝;⌜b⌝;⌜E⌝;⌜d⌝;⌜f⌝]⋅ THENA EAuto  1)
          THEN D 0 With ⌜f⌝ 
          THEN Auto)) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. bca < abc
7. d : Point
8. b=d=c
9. d # ba
10. E : Point
11. a=d=E
12. bE ≅ ca
13. dbE < abd
14. ∃f:Point. ((abf ≅a Ebf ∧ a-f-E) ∧ |af| < |Ef|)
⊢ |ab| < |ac|

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  a  \#  bc
6.  bca  <  abc
7.  d  :  Point
8.  b=d=c
9.  d  \#  ba
10.  E  :  Point
11.  a=d=E
12.  bE  \mcong{}  ca
13.  dbE  <  abd
\mvdash{}  |ab|  <  |ac|


By

---

Latex:
(Assert  \mexists{}f:Point.  ((abf  \mcong{}\msuba{}  Ebf  \mwedge{}  a-f-E)  \mwedge{}  |af|  <  |Ef|)  BY
              ((InstLemma  `Euclid-Prop9-with-between`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}E\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THEN  Auto)
                THEN  ExRepD
                THEN  (InstLemma  `Euclid-Prop19-lemma2`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}E\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  EAuto    1)
                THEN  D  0  With  \mkleeneopen{}f\mkleeneclose{} 
                THEN  Auto))

---

Home Index