---

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


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)
BY
{ (((gProperProlong ⌜b⌝⌜a⌝`c1\''⌜a⌝⌜c1⌝⋅ THENA Auto) THEN (gProperProlong ⌜a⌝⌜b⌝`c2\''⌜b⌝⌜c2⌝⋅ THENA Auto) THEN ExRepD)
   THEN (gProlong ⌜a⌝⌜b⌝`c1\'\''⌜b⌝⌜c1⌝⋅ THENA Auto)
   THEN (gProlong ⌜b⌝⌜a⌝`c2\'\''⌜a⌝⌜c2⌝⋅ 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
19. ac1 ≅ ac
20. c2 : Point
21. y-b-c2
22. bc2 ≅ bc
23. c1' : Point
24. b-a-c1'
25. ac1' ≅ ac1
26. c2' : Point
27. a-b-c2'
28. bc2' ≅ bc2
29. c1'' : Point
30. a_b_c1'' ∧ bc1'' ≅ bc1
31. c2'' : Point
32. b_a_c2'' ∧ ac2'' ≅ ac2
⊢ ∃c1,c2:Point. ((ac ≅ ac1 ∧ bc2 > bc1) ∧ bc ≅ bc2 ∧ ac1 > ac2)

---

Latex:

---

Latex:

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  \mneq{}  b
9.  b  \mneq{}  c
10.  c  \mneq{}  a
11.  x  :  Point
12.  b-a-x
13.  ax  \mcong{}  OX
14.  y  :  Point
15.  a-b-y
16.  by  \mcong{}  OX
17.  c1  :  Point
18.  x-a-c1  \mwedge{}  ac1  \mcong{}  ac
19.  c2  :  Point
20.  y-b-c2  \mwedge{}  bc2  \mcong{}  bc
\mvdash{}  \mexists{}c1,c2:Point.  ((ac  \mcong{}  ac1  \mwedge{}  bc2  >  bc1)  \mwedge{}  bc  \mcong{}  bc2  \mwedge{}  ac1  >  ac2)


By

---

Latex:
(((gProperProlong  \mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}`c1\mbackslash{}''\mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}c1\mkleeneclose{}\mcdot{}  THENA  Auto)
    THEN  (gProperProlong  \mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}b\mkleeneclose{}`c2\mbackslash{}''\mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}c2\mkleeneclose{}\mcdot{}  THENA  Auto)
    THEN  ExRepD)
  THEN  (gProlong  \mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}b\mkleeneclose{}`c1\mbackslash{}'\mbackslash{}''\mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}c1\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (gProlong  \mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}`c2\mbackslash{}'\mbackslash{}''\mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}c2\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index