---

Step * 1 1 1 1 2 1 1 1 1 of Lemma Prop23-construction-lemma


1. e : EuclideanPlane
2. p : Point
3. q : Point
4. r : Point
5. a : Point
6. a' : Point
7. p # qr
8. a ≠ a'
9. |qr| < |qp| + |pr|
10. |pr| < |qp| + |qr|
11. |qp| < |pr| + |qr|
12. P : Point
13. a'-a-P
14. aP ≅ OX
15. b : Point
16. P-a-b
17. ab ≅ pq
18. out(a a'b)
19. c1 : Point
20. c1' : Point
21. c1'' : Point
22. c2 : Point
23. c2' : Point
24. c2'' : Point
25. pc1 ≅ pr
26. out(p qc1)
27. qc2 ≅ qr
28. out(q pc2)
29. q-p-c1'
30. pc1' ≅ pc1
31. p-q-c2'
32. qc2' ≅ qc2
33. p_q_c1''
34. qc1'' ≅ qc1
35. q_p_c2''
36. pc2'' ≅ pc2
37. p-c1-c2'
38. q-c2-c1'
39. c1'-p-c1
40. c2'-q-c2
41. c1'-c2-c2'
42. c2'-c1-c1'
43. c1'-c2-c1
44. c2'-c1-c2
45. C1' : Point
46. b-a-C1'
47. aC1' ≅ pc1
48. C2' : Point
49. a-b-C2'
50. bC2' ≅ qc2
51. C1 : Point
52. C1'_a_C1
53. C1' ≠ a
54. a ≠ C1
55. aC1 ≅ C1'a
56. C2 : Point
57. C2'-b-C2
58. bC2 ≅ C2'b
59. C1'' : Point
60. a_b_C1''
61. bC1'' ≅ bC1
62. C2'' : Point
63. b_a_C2''
64. aC2'' ≅ aC2
65. a-C1-C2'
66. C1'-C2-C2'
67. out(C1' C2C1)
68. |C1'C2| < |C1'C1| ⇒ |C1'C2| + |C2b| < |C1'C1| + |C2b|
69. |C1'C2| + |C2b| = |C1'a| + |ab| ∈ Length
70. |C1'a| = |pr| ∈ Length
71. |C1'C1| = |C1'a| + |aC1| ∈ Length
72. |C1'a| + |aC1| + |C2b| = |pr| + |pr| + |qr| ∈ Length
73. |pr| + |pr| + |qr| = |pr| + |pr| + |qr| ∈ Length
⊢ |pr| + |ab| < |pr| + |pr| + |qr|
BY
{ ((InstLemma `geo-lt-add1-iff` [⌜e⌝;⌜|pq|⌝;⌜|pr| + |qr|⌝;⌜|pr|⌝]⋅ THEN Auto)
   THEN ((InstLemma `geo-zero-point-sep-iff-sep` [⌜e⌝;⌜p⌝;⌜r⌝]⋅ THEN Auto)
         THEN InstLemma `geo-zero-point-sep-iff-sep` [⌜e⌝;⌜p⌝;⌜q⌝]⋅
         THEN Auto)
   THEN (InstLemma `geo-lt-sep` [⌜e⌝;⌜q⌝;⌜p⌝;⌜X⌝;⌜|pr| + |qr|⌝]⋅ THEN Auto)
   THEN (Assert |qr| = |pq| ∈ Length BY
               Auto)
   THEN RWO "-1" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  p  :  Point
3.  q  :  Point
4.  r  :  Point
5.  a  :  Point
6.  a'  :  Point
7.  p  \#  qr
8.  a  \mneq{}  a'
9.  |qr|  <  |qp|  +  |pr|
10.  |pr|  <  |qp|  +  |qr|
11.  |qp|  <  |pr|  +  |qr|
12.  P  :  Point
13.  a'-a-P
14.  aP  \mcong{}  OX
15.  b  :  Point
16.  P-a-b
17.  ab  \mcong{}  pq
18.  out(a  a'b)
19.  c1  :  Point
20.  c1'  :  Point
21.  c1''  :  Point
22.  c2  :  Point
23.  c2'  :  Point
24.  c2''  :  Point
25.  pc1  \mcong{}  pr
26.  out(p  qc1)
27.  qc2  \mcong{}  qr
28.  out(q  pc2)
29.  q-p-c1'
30.  pc1'  \mcong{}  pc1
31.  p-q-c2'
32.  qc2'  \mcong{}  qc2
33.  p\_q\_c1''
34.  qc1''  \mcong{}  qc1
35.  q\_p\_c2''
36.  pc2''  \mcong{}  pc2
37.  p-c1-c2'
38.  q-c2-c1'
39.  c1'-p-c1
40.  c2'-q-c2
41.  c1'-c2-c2'
42.  c2'-c1-c1'
43.  c1'-c2-c1
44.  c2'-c1-c2
45.  C1'  :  Point
46.  b-a-C1'
47.  aC1'  \mcong{}  pc1
48.  C2'  :  Point
49.  a-b-C2'
50.  bC2'  \mcong{}  qc2
51.  C1  :  Point
52.  C1'\_a\_C1
53.  C1'  \mneq{}  a
54.  a  \mneq{}  C1
55.  aC1  \mcong{}  C1'a
56.  C2  :  Point
57.  C2'-b-C2
58.  bC2  \mcong{}  C2'b
59.  C1''  :  Point
60.  a\_b\_C1''
61.  bC1''  \mcong{}  bC1
62.  C2''  :  Point
63.  b\_a\_C2''
64.  aC2''  \mcong{}  aC2
65.  a-C1-C2'
66.  C1'-C2-C2'
67.  out(C1'  C2C1)
68.  |C1'C2|  <  |C1'C1|  {}\mRightarrow{}  |C1'C2|  +  |C2b|  <  |C1'C1|  +  |C2b|
69.  |C1'C2|  +  |C2b|  =  |C1'a|  +  |ab|
70.  |C1'a|  =  |pr|
71.  |C1'C1|  =  |C1'a|  +  |aC1|
72.  |C1'a|  +  |aC1|  +  |C2b|  =  |pr|  +  |pr|  +  |qr|
73.  |pr|  +  |pr|  +  |qr|  =  |pr|  +  |pr|  +  |qr|
\mvdash{}  |pr|  +  |ab|  <  |pr|  +  |pr|  +  |qr|


By

---

Latex:
((InstLemma  `geo-lt-add1-iff`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}|pq|\mkleeneclose{};\mkleeneopen{}|pr|  +  |qr|\mkleeneclose{};\mkleeneopen{}|pr|\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  ((InstLemma  `geo-zero-point-sep-iff-sep`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THEN  Auto)
              THEN  InstLemma  `geo-zero-point-sep-iff-sep`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}
              THEN  Auto)
  THEN  (InstLemma  `geo-lt-sep`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}|pr|  +  |qr|\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  (Assert  |qr|  =  |pq|  BY
                          Auto)
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index