---

Step * 1 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
14. ∃f:Point. ((abf ≅a Ebf ∧ a-f-E) ∧ |af| < |Ef|)
⊢ |ab| < |ac|
BY
{ (ExRepD
   THEN (InstLemma `Euclid-Prop19-lemma1` [⌜e⌝;⌜b⌝;⌜a⌝;⌜E⌝;⌜f⌝]⋅ THENA Auto)
   THEN (Assert |bE| = |ac| ∈ Length BY
               EAuto 1)
   THEN RWO "-1" (-2)
   THEN EAuto 1) }

---

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
14.  \mexists{}f:Point.  ((abf  \mcong{}\msuba{}  Ebf  \mwedge{}  a-f-E)  \mwedge{}  |af|  <  |Ef|)
\mvdash{}  |ab|  <  |ac|


By

---

Latex:
(ExRepD
  THEN  (InstLemma  `Euclid-Prop19-lemma1`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}E\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  |bE|  =  |ac|  BY
                          EAuto  1)
  THEN  RWO  "-1"  (-2)
  THEN  EAuto  1)

---

Home Index