---

Step * 1 of Lemma Prop22-symmetric-point-construction-lemma


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. |bc| < |ba| + |ac|
7. |ac| < |ba| + |bc|
8. |ba| < |ac| + |bc|
9. a ≠ b
10. b ≠ c
11. c ≠ a
12. x : Point
13. b-a-x
14. ax ≅ OX
15. y : Point
16. a-b-y
17. by ≅ OX
18. c1 : Point
19. x-a-c1 ∧ ac1 ≅ ac
20. c2 : Point
21. y-b-c2 ∧ bc2 ≅ bc
⊢ ∃c1,c1',c1'',c2,c2',c2'':Point
   ((ac1 ≅ ac ∧ out(a bc1))
   ∧ (bc2 ≅ bc ∧ out(b ac2))
   ∧ (b-a-c1' ∧ ac1' ≅ ac1)
   ∧ (a-b-c2' ∧ bc2' ≅ bc2)
   ∧ (a_b_c1'' ∧ bc1'' ≅ bc1)
   ∧ (b_a_c2'' ∧ ac2'' ≅ ac2)
   ∧ (a-c1-c2' ∧ b-c2-c1')
   ∧ (c1'-a-c1 ∧ c2'-b-c2)
   ∧ (c1'-c2-c2' ∧ c2'-c1-c1')
   ∧ c1'-c2-c1
   ∧ c2'-c1-c2)
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. a # bc
6. |bc| < |ba| + |ac|
7. |ac| < |ba| + |bc|
8. |ba| < |ac| + |bc|
9. a ≠ b
10. b ≠ c
11. c ≠ a
12. x : Point
13. b-a-x
14. ax ≅ OX
15. y : Point
16. a-b-y
17. by ≅ OX
18. c1 : Point
19. x-a-c1
20. ac1 ≅ ac
21. c2 : Point
22. y-b-c2
23. bc2 ≅ bc
24. c1' : Point
25. b-a-c1'
26. ac1' ≅ ac1
27. c2' : Point
28. a-b-c2'
29. bc2' ≅ bc2
30. c1'' : Point
31. a_b_c1'' ∧ bc1'' ≅ bc1
32. c2'' : Point
33. b_a_c2'' ∧ ac2'' ≅ ac2
⊢ ∃c1,c1',c1'',c2,c2',c2'':Point
   ((ac1 ≅ ac ∧ out(a bc1))
   ∧ (bc2 ≅ bc ∧ out(b ac2))
   ∧ (b-a-c1' ∧ ac1' ≅ ac1)
   ∧ (a-b-c2' ∧ bc2' ≅ bc2)
   ∧ (a_b_c1'' ∧ bc1'' ≅ bc1)
   ∧ (b_a_c2'' ∧ ac2'' ≅ ac2)
   ∧ (a-c1-c2' ∧ b-c2-c1')
   ∧ (c1'-a-c1 ∧ c2'-b-c2)
   ∧ (c1'-c2-c2' ∧ c2'-c1-c1')
   ∧ c1'-c2-c1
   ∧ c2'-c1-c2)

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  a  \#  bc
6.  |bc|  <  |ba|  +  |ac|
7.  |ac|  <  |ba|  +  |bc|
8.  |ba|  <  |ac|  +  |bc|
9.  a  \mneq{}  b
10.  b  \mneq{}  c
11.  c  \mneq{}  a
12.  x  :  Point
13.  b-a-x
14.  ax  \mcong{}  OX
15.  y  :  Point
16.  a-b-y
17.  by  \mcong{}  OX
18.  c1  :  Point
19.  x-a-c1  \mwedge{}  ac1  \mcong{}  ac
20.  c2  :  Point
21.  y-b-c2  \mwedge{}  bc2  \mcong{}  bc
\mvdash{}  \mexists{}c1,c1',c1'',c2,c2',c2'':Point
      ((ac1  \mcong{}  ac  \mwedge{}  out(a  bc1))
      \mwedge{}  (bc2  \mcong{}  bc  \mwedge{}  out(b  ac2))
      \mwedge{}  (b-a-c1'  \mwedge{}  ac1'  \mcong{}  ac1)
      \mwedge{}  (a-b-c2'  \mwedge{}  bc2'  \mcong{}  bc2)
      \mwedge{}  (a\_b\_c1''  \mwedge{}  bc1''  \mcong{}  bc1)
      \mwedge{}  (b\_a\_c2''  \mwedge{}  ac2''  \mcong{}  ac2)
      \mwedge{}  (a-c1-c2'  \mwedge{}  b-c2-c1')
      \mwedge{}  (c1'-a-c1  \mwedge{}  c2'-b-c2)
      \mwedge{}  (c1'-c2-c2'  \mwedge{}  c2'-c1-c1')
      \mwedge{}  c1'-c2-c1
      \mwedge{}  c2'-c1-c2)


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