---

Step * of Lemma Euclid-Prop22

No Annotations
∀e:EuclideanPlane. ∀a1,a2,b1,b2,c1,c2:Point.
  (|a1a2| < |b1b2| + |c1c2|
  ⇒ |b1b2| < |a1a2| + |c1c2|
  ⇒ |c1c2| < |a1a2| + |b1b2|
  ⇒ (∃a,b,c:Point. (((a # bc ∧ ab ≅ a1a2) ∧ bc ≅ b1b2) ∧ ca ≅ c1c2)))
BY
{ ((Auto
    THEN (Assert a1 # a2 ∧ b1 # b2 ∧ c1 # c2 BY
                (InstLemma `geo-triangle-inequality-lt-sep` [⌜e⌝;⌜a1⌝;⌜a2⌝;⌜b1⌝;⌜b2⌝;⌜c1⌝;⌜c2⌝]⋅ THEN Auto))
    THEN ExRepD)
   THEN ((gProperProlong ⌜O⌝⌜X⌝`f'⌜a1⌝⌜a2⌝⋅ THENA Auto) THEN ExRepD)
   THEN ((gProperProlong ⌜X⌝⌜f⌝`g'⌜b1⌝⌜b2⌝⋅ THENA Auto) THEN ExRepD)
   THEN (gProperProlong ⌜f⌝⌜g⌝`h'⌜c1⌝⌜c2⌝⋅ THENA Auto)
   THEN ExRepD) }

1
1. e : EuclideanPlane
2. a1 : Point
3. a2 : Point
4. b1 : Point
5. b2 : Point
6. c1 : Point
7. c2 : Point
8. |a1a2| < |b1b2| + |c1c2|
9. |b1b2| < |a1a2| + |c1c2|
10. |c1c2| < |a1a2| + |b1b2|
11. a1 # a2
12. b1 # b2
13. c1 # c2
14. f : Point
15. O-X-f
16. Xf ≅ a1a2
17. g : Point
18. X-f-g
19. fg ≅ b1b2
20. h : Point
21. f-g-h
22. gh ≅ c1c2
⊢ ∃a,b,c:Point. (((a # bc ∧ ab ≅ a1a2) ∧ bc ≅ b1b2) ∧ ca ≅ c1c2)

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a1,a2,b1,b2,c1,c2:Point.
    (|a1a2|  <  |b1b2|  +  |c1c2|
    {}\mRightarrow{}  |b1b2|  <  |a1a2|  +  |c1c2|
    {}\mRightarrow{}  |c1c2|  <  |a1a2|  +  |b1b2|
    {}\mRightarrow{}  (\mexists{}a,b,c:Point.  (((a  \#  bc  \mwedge{}  ab  \mcong{}  a1a2)  \mwedge{}  bc  \mcong{}  b1b2)  \mwedge{}  ca  \mcong{}  c1c2)))


By

---

Latex:
((Auto
    THEN  (Assert  a1  \#  a2  \mwedge{}  b1  \#  b2  \mwedge{}  c1  \#  c2  BY
                            (InstLemma  `geo-triangle-inequality-lt-sep`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{};\mkleeneopen{}a2\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{};\mkleeneopen{}b2\mkleeneclose{};\mkleeneopen{}c1\mkleeneclose{};\mkleeneopen{}c2\mkleeneclose{}]\mcdot{}
                              THEN  Auto
                              ))
    THEN  ExRepD)
  THEN  ((gProperProlong  \mkleeneopen{}O\mkleeneclose{}\mkleeneopen{}X\mkleeneclose{}`f'\mkleeneopen{}a1\mkleeneclose{}\mkleeneopen{}a2\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ExRepD)
  THEN  ((gProperProlong  \mkleeneopen{}X\mkleeneclose{}\mkleeneopen{}f\mkleeneclose{}`g'\mkleeneopen{}b1\mkleeneclose{}\mkleeneopen{}b2\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ExRepD)
  THEN  (gProperProlong  \mkleeneopen{}f\mkleeneclose{}\mkleeneopen{}g\mkleeneclose{}`h'\mkleeneopen{}c1\mkleeneclose{}\mkleeneopen{}c2\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ExRepD)

---

Home Index