Step
*
1
1
1
1
1
1
1
1
of Lemma
hp-angle-sum-eq3
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. i : Point
9. j : Point
10. k : Point
11. a' : Point
12. b' : Point
13. c' : Point
14. x' : Point
15. y' : Point
16. z' : Point
17. i' : Point
18. j' : Point
19. k' : Point
20. abc ≅a a'b'c'
21. ijk ≅a i'j'k'
22. p1 : Point
23. p2 : Point
24. d1 : Point
25. f1 : Point
26. abc ≅a ijp1
27. kjp1 ≅a xyz
28. B(jp2p1)
29. out(j id1)
30. out(j kf1)
31. d1-p2-f1
32. p : Point
33. p' : Point
34. d' : Point
35. f' : Point
36. a'b'c' ≅a i'j'p
37. k'j'p ≅a x'y'z'
38. B(j'p'p)
39. out(j' i'd')
40. out(j' k'f')
41. d'-p'-f'
42. a # bc
43. i # jk
44. A1 : Point
45. d1-j-A1
46. jA1 ≅ OX
47. B1 : Point
48. f1-j-B1
49. jB1 ≅ OX
50. A2 : Point
51. d'-j'-A2
52. j'A2 ≅ OX
53. B2 : Point
54. f'-j'-B2
55. j'B2 ≅ OX
56. C1 : Point
57. A1-j-C1
58. jC1 ≅ OX
59. D1 : Point
60. B1-j-D1
61. jD1 ≅ OX
62. C2 : Point
63. A2-j'-C2
64. j'C2 ≅ OX
65. D2 : Point
66. B2-j'-D2
67. j'D2 ≅ OX
68. d1 # jf1
69. out(j d1C1)
70. out(j f1D1)
71. d' # j'f'
72. out(j' d'C2)
73. out(j' f'D2)
74. x1 : Point
75. C1-x1-D1
76. out(j p2x1)
77. d1jp2 ≅a C1jx1
78. f1jp2 ≅a D1jx1
79. J1 : Point
80. p-j'-J1
81. j'J1 ≅ OX
82. x2 : Point
83. J1-j'-x2
84. j'x2 ≅ jx1
85. out(j' px2)
⊢ xyz ≅a x'y'z'
BY
{ ((Assert out(j' i'C2) BY
(InstLemma `geo-out_transitivity` [⌜e⌝;⌜j'⌝;⌜i'⌝;⌜d'⌝;⌜C2⌝]⋅ THEN EAuto 1))
THEN (Assert out(j' k'D2) BY
(InstLemma `geo-out_transitivity` [⌜e⌝;⌜j'⌝;⌜k'⌝;⌜f'⌝;⌜D2⌝]⋅ THEN EAuto 1))
THEN (Assert out(j iC1) BY
(InstLemma `geo-out_transitivity` [⌜e⌝;⌜j⌝;⌜i⌝;⌜d1⌝;⌜C1⌝]⋅ THEN EAuto 1))
THEN (Assert out(j kD1) BY
(InstLemma `geo-out_transitivity` [⌜e⌝;⌜j⌝;⌜k⌝;⌜f1⌝;⌜D1⌝]⋅ THEN EAuto 1))) }
1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. i : Point
9. j : Point
10. k : Point
11. a' : Point
12. b' : Point
13. c' : Point
14. x' : Point
15. y' : Point
16. z' : Point
17. i' : Point
18. j' : Point
19. k' : Point
20. abc ≅a a'b'c'
21. ijk ≅a i'j'k'
22. p1 : Point
23. p2 : Point
24. d1 : Point
25. f1 : Point
26. abc ≅a ijp1
27. kjp1 ≅a xyz
28. B(jp2p1)
29. out(j id1)
30. out(j kf1)
31. d1-p2-f1
32. p : Point
33. p' : Point
34. d' : Point
35. f' : Point
36. a'b'c' ≅a i'j'p
37. k'j'p ≅a x'y'z'
38. B(j'p'p)
39. out(j' i'd')
40. out(j' k'f')
41. d'-p'-f'
42. a # bc
43. i # jk
44. A1 : Point
45. d1-j-A1
46. jA1 ≅ OX
47. B1 : Point
48. f1-j-B1
49. jB1 ≅ OX
50. A2 : Point
51. d'-j'-A2
52. j'A2 ≅ OX
53. B2 : Point
54. f'-j'-B2
55. j'B2 ≅ OX
56. C1 : Point
57. A1-j-C1
58. jC1 ≅ OX
59. D1 : Point
60. B1-j-D1
61. jD1 ≅ OX
62. C2 : Point
63. A2-j'-C2
64. j'C2 ≅ OX
65. D2 : Point
66. B2-j'-D2
67. j'D2 ≅ OX
68. d1 # jf1
69. out(j d1C1)
70. out(j f1D1)
71. d' # j'f'
72. out(j' d'C2)
73. out(j' f'D2)
74. x1 : Point
75. C1-x1-D1
76. out(j p2x1)
77. d1jp2 ≅a C1jx1
78. f1jp2 ≅a D1jx1
79. J1 : Point
80. p-j'-J1
81. j'J1 ≅ OX
82. x2 : Point
83. J1-j'-x2
84. j'x2 ≅ jx1
85. out(j' px2)
86. out(j' i'C2)
87. out(j' k'D2)
88. out(j iC1)
89. out(j kD1)
⊢ xyz ≅a x'y'z'
Latex:
Latex:
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. i : Point
9. j : Point
10. k : Point
11. a' : Point
12. b' : Point
13. c' : Point
14. x' : Point
15. y' : Point
16. z' : Point
17. i' : Point
18. j' : Point
19. k' : Point
20. abc \mcong{}\msuba{} a'b'c'
21. ijk \mcong{}\msuba{} i'j'k'
22. p1 : Point
23. p2 : Point
24. d1 : Point
25. f1 : Point
26. abc \mcong{}\msuba{} ijp1
27. kjp1 \mcong{}\msuba{} xyz
28. B(jp2p1)
29. out(j id1)
30. out(j kf1)
31. d1-p2-f1
32. p : Point
33. p' : Point
34. d' : Point
35. f' : Point
36. a'b'c' \mcong{}\msuba{} i'j'p
37. k'j'p \mcong{}\msuba{} x'y'z'
38. B(j'p'p)
39. out(j' i'd')
40. out(j' k'f')
41. d'-p'-f'
42. a \# bc
43. i \# jk
44. A1 : Point
45. d1-j-A1
46. jA1 \mcong{} OX
47. B1 : Point
48. f1-j-B1
49. jB1 \mcong{} OX
50. A2 : Point
51. d'-j'-A2
52. j'A2 \mcong{} OX
53. B2 : Point
54. f'-j'-B2
55. j'B2 \mcong{} OX
56. C1 : Point
57. A1-j-C1
58. jC1 \mcong{} OX
59. D1 : Point
60. B1-j-D1
61. jD1 \mcong{} OX
62. C2 : Point
63. A2-j'-C2
64. j'C2 \mcong{} OX
65. D2 : Point
66. B2-j'-D2
67. j'D2 \mcong{} OX
68. d1 \# jf1
69. out(j d1C1)
70. out(j f1D1)
71. d' \# j'f'
72. out(j' d'C2)
73. out(j' f'D2)
74. x1 : Point
75. C1-x1-D1
76. out(j p2x1)
77. d1jp2 \mcong{}\msuba{} C1jx1
78. f1jp2 \mcong{}\msuba{} D1jx1
79. J1 : Point
80. p-j'-J1
81. j'J1 \mcong{} OX
82. x2 : Point
83. J1-j'-x2
84. j'x2 \mcong{} jx1
85. out(j' px2)
\mvdash{} xyz \mcong{}\msuba{} x'y'z'
By
Latex:
((Assert out(j' i'C2) BY
(InstLemma `geo-out\_transitivity` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}j'\mkleeneclose{};\mkleeneopen{}i'\mkleeneclose{};\mkleeneopen{}d'\mkleeneclose{};\mkleeneopen{}C2\mkleeneclose{}]\mcdot{} THEN EAuto 1))
THEN (Assert out(j' k'D2) BY
(InstLemma `geo-out\_transitivity` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}j'\mkleeneclose{};\mkleeneopen{}k'\mkleeneclose{};\mkleeneopen{}f'\mkleeneclose{};\mkleeneopen{}D2\mkleeneclose{}]\mcdot{} THEN EAuto 1))
THEN (Assert out(j iC1) BY
(InstLemma `geo-out\_transitivity` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}d1\mkleeneclose{};\mkleeneopen{}C1\mkleeneclose{}]\mcdot{} THEN EAuto 1))
THEN (Assert out(j kD1) BY
(InstLemma `geo-out\_transitivity` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}f1\mkleeneclose{};\mkleeneopen{}D1\mkleeneclose{}]\mcdot{} THEN EAuto 1)))
Home
Index