Step
*
1
1
1
1
2
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. aC1 ≅ C1'a
54. C2 : Point
55. C2'-b-C2
56. bC2 ≅ C2'b
57. C1'' : Point
58. a_b_C1''
59. bC1'' ≅ bC1
60. C2'' : Point
61. b_a_C2''
62. aC2'' ≅ aC2
63. a-C1-C2'
64. C1'-C2-C2'
65. out(C1' C2C1)
66. |C1'C2| < |C1'C1| ⇒ |C1'C2| + |C2b| < |C1'C1| + |C2b|
67. |C1'C2| + |C2b| = |C1'a| + |ab| ∈ Length
⊢ |C1'C2| + |C2b| < |C1'C1| + |C2b|
BY
{ (((((RWO "-1" 0 THEN Auto) THEN (Assert |C1'a| = |pr| ∈ Length BY Auto)) THEN RWO "-1" 0 THEN Auto)
THEN ((D 52 THEN FLemma `geo-add-length-between` [52]) THEN Auto)
THEN RWO "-1" 0
THEN Auto)
THEN (Assert |C1'a| + |aC1| + |C2b| = |pr| + |pr| + |qr| ∈ Length BY
Auto)
THEN ((Assert |pr| + |pr| + |qr| = |pr| + |pr| + |qr| ∈ Length BY Auto) THEN RWO "-1" 72 THEN Auto)
THEN RWO "-2" 0
THEN Auto) }
1
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|
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. aC1 \mcong{} C1'a
54. C2 : Point
55. C2'-b-C2
56. bC2 \mcong{} C2'b
57. C1'' : Point
58. a\_b\_C1''
59. bC1'' \mcong{} bC1
60. C2'' : Point
61. b\_a\_C2''
62. aC2'' \mcong{} aC2
63. a-C1-C2'
64. C1'-C2-C2'
65. out(C1' C2C1)
66. |C1'C2| < |C1'C1| {}\mRightarrow{} |C1'C2| + |C2b| < |C1'C1| + |C2b|
67. |C1'C2| + |C2b| = |C1'a| + |ab|
\mvdash{} |C1'C2| + |C2b| < |C1'C1| + |C2b|
By
Latex:
(((((RWO "-1" 0 THEN Auto) THEN (Assert |C1'a| = |pr| BY Auto)) THEN RWO "-1" 0 THEN Auto)
THEN ((D 52 THEN FLemma `geo-add-length-between` [52]) THEN Auto)
THEN RWO "-1" 0
THEN Auto)
THEN (Assert |C1'a| + |aC1| + |C2b| = |pr| + |pr| + |qr| BY
Auto)
THEN ((Assert |pr| + |pr| + |qr| = |pr| + |pr| + |qr| BY Auto) THEN RWO "-1" 72 THEN Auto)
THEN RWO "-2" 0
THEN Auto)
Home
Index