---

Step * of Lemma Prop22-inequality-to-triangle-construction

∀e:EuclideanPlane. ∀a,b,c:Point.
  (|ac| < |ab| + |bc|
  ⇒ |ab| < |ac| + |bc|
  ⇒ |bc| < |ac| + |ab|
  ⇒ (∃c1,c2:Point. ((ac ≅ ac1 ∧ bc2 > bc1) ∧ bc ≅ bc2 ∧ ac1 > ac2)))
BY
{ (Auto
   THEN ((Assert a ≠ b ∧ b ≠ c ∧ c ≠ a BY
                (InstLemma `geo-triangle-inequality-lt-sep` [⌜e⌝;⌜a⌝;⌜b⌝;⌜b⌝;⌜c⌝;⌜a⌝;⌜c⌝]⋅ THEN Auto))
         THEN ExRepD
         )
   THEN (gProperProlong ⌜b⌝⌜a⌝`x'⌜O⌝⌜X⌝⋅ THENA Auto)
   THEN ((gProperProlong ⌜a⌝⌜b⌝`y'⌜O⌝⌜X⌝⋅ THENA Auto) THEN ExRepD)
   THEN (gProperProlong ⌜x⌝⌜a⌝`c1'⌜a⌝⌜c⌝⋅ THENA Auto)
   THEN (gProperProlong ⌜y⌝⌜b⌝`c2'⌜b⌝⌜c⌝⋅ THENA Auto)) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. |ac| < |ab| + |bc|
6. |ab| < |ac| + |bc|
7. |bc| < |ac| + |ab|
8. a ≠ b
9. b ≠ c
10. c ≠ a
11. x : Point
12. b-a-x
13. ax ≅ OX
14. y : Point
15. a-b-y
16. by ≅ OX
17. c1 : Point
18. x-a-c1 ∧ ac1 ≅ ac
19. c2 : Point
20. y-b-c2 ∧ bc2 ≅ bc
⊢ ∃c1,c2:Point. ((ac ≅ ac1 ∧ bc2 > bc1) ∧ bc ≅ bc2 ∧ ac1 > ac2)

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c:Point.
    (|ac|  <  |ab|  +  |bc|
    {}\mRightarrow{}  |ab|  <  |ac|  +  |bc|
    {}\mRightarrow{}  |bc|  <  |ac|  +  |ab|
    {}\mRightarrow{}  (\mexists{}c1,c2:Point.  ((ac  \mcong{}  ac1  \mwedge{}  bc2  >  bc1)  \mwedge{}  bc  \mcong{}  bc2  \mwedge{}  ac1  >  ac2)))


By

---

Latex:
(Auto
  THEN  ((Assert  a  \mneq{}  b  \mwedge{}  b  \mneq{}  c  \mwedge{}  c  \mneq{}  a  BY
                            (InstLemma  `geo-triangle-inequality-lt-sep`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THEN  Auto))
              THEN  ExRepD
              )
  THEN  (gProperProlong  \mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}`x'\mkleeneopen{}O\mkleeneclose{}\mkleeneopen{}X\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ((gProperProlong  \mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}b\mkleeneclose{}`y'\mkleeneopen{}O\mkleeneclose{}\mkleeneopen{}X\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ExRepD)
  THEN  (gProperProlong  \mkleeneopen{}x\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}`c1'\mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}c\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (gProperProlong  \mkleeneopen{}y\mkleeneclose{}\mkleeneopen{}b\mkleeneclose{}`c2'\mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}c\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index