Step
*
1
2
1
1
2
of Lemma
geo-cong-angle-transitivity
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. p : Point
9. q : Point
10. r : Point
11. a # b
12. c # b
13. x # y
14. z # y
15. p # q
16. r # q
17. a # b
18. b # c
19. x # y
20. y # z
21. a1 : Point
22. c1 : Point
23. x1 : Point
24. z1 : Point
25. B(baa1)
26. B(bcc1)
27. B(yxx1)
28. B(yzz1)
29. ba1 ≅ yx1
30. bc1 ≅ yz1
31. a1c1 ≅ x1z1
32. x # y
33. y # z
34. p # q
35. q # r
36. a' : Point
37. c' : Point
38. x' : Point
39. z' : Point
40. B(yxa')
41. B(yzc')
42. B(qpx')
43. B(qrz')
44. ya' ≅ qx'
45. yc' ≅ qz'
46. a'c' ≅ x'z'
47. A : Point
48. B(ba1A)
49. a1A ≅ qx'
50. X : Point
51. B(qx'X)
52. x'X ≅ ba1
53. C : Point
54. B(bc1C)
55. c1C ≅ qz'
56. Z : Point
57. B(qz'Z)
58. z'Z ≅ bc1
59. B(baA)
60. B(bcC)
61. B(qpX)
62. B(qrZ)
63. bA ≅ qX
64. bC ≅ qZ
65. B(qpX)
66. B(qrZ)
67. bA ≅ qX
68. bC ≅ qZ
69. X0 : Point
70. Z0 : Point
71. B(bX0a1)
72. B(bZ0c1)
73. yx ≅ bX0
74. xx1 ≅ X0a1
75. yz ≅ bZ0
76. zz1 ≅ Z0c1
77. X0Z0 ≅ xz
78. ∃X1,Z1:Point. ((B(qX1x') ∧ B(qZ1z')) ∧ yx ≅ qX1 ∧ (xa' ≅ X1x' ∧ yz ≅ qZ1) ∧ zc' ≅ Z1z')
⊢ AC ≅ XZ
BY
{ (ExRepD
THEN (Assert X1Z1 ≅ xz BY
(InstLemma `geo-inner-five-segment` [⌜e⌝;⌜y⌝;⌜z⌝;⌜c'⌝;⌜x⌝;⌜q⌝;⌜Z1⌝;⌜z'⌝;⌜X1⌝]⋅ THEN Auto))
THEN InstLemma `geo-inner-five-segment` [⌜e⌝;⌜y⌝;⌜x⌝;⌜a'⌝;⌜c'⌝;⌜q⌝;⌜X1⌝;⌜x'⌝;⌜z'⌝]⋅
THEN Auto) }
1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. p : Point
9. q : Point
10. r : Point
11. a # b
12. c # b
13. x # y
14. z # y
15. p # q
16. r # q
17. a # b
18. b # c
19. x # y
20. y # z
21. a1 : Point
22. c1 : Point
23. x1 : Point
24. z1 : Point
25. B(baa1)
26. B(bcc1)
27. B(yxx1)
28. B(yzz1)
29. ba1 ≅ yx1
30. bc1 ≅ yz1
31. a1c1 ≅ x1z1
32. x # y
33. y # z
34. p # q
35. q # r
36. a' : Point
37. c' : Point
38. x' : Point
39. z' : Point
40. B(yxa')
41. B(yzc')
42. B(qpx')
43. B(qrz')
44. ya' ≅ qx'
45. yc' ≅ qz'
46. a'c' ≅ x'z'
47. A : Point
48. B(ba1A)
49. a1A ≅ qx'
50. X : Point
51. B(qx'X)
52. x'X ≅ ba1
53. C : Point
54. B(bc1C)
55. c1C ≅ qz'
56. Z : Point
57. B(qz'Z)
58. z'Z ≅ bc1
59. B(baA)
60. B(bcC)
61. B(qpX)
62. B(qrZ)
63. bA ≅ qX
64. bC ≅ qZ
65. B(qpX)
66. B(qrZ)
67. bA ≅ qX
68. bC ≅ qZ
69. X0 : Point
70. Z0 : Point
71. B(bX0a1)
72. B(bZ0c1)
73. yx ≅ bX0
74. xx1 ≅ X0a1
75. yz ≅ bZ0
76. zz1 ≅ Z0c1
77. X0Z0 ≅ xz
78. X1 : Point
79. Z1 : Point
80. B(qX1x')
81. B(qZ1z')
82. yx ≅ qX1
83. xa' ≅ X1x'
84. yz ≅ qZ1
85. zc' ≅ Z1z'
86. X1Z1 ≅ xz
87. xc' ≅ X1z'
⊢ AC ≅ XZ
Latex:
Latex:
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. p : Point
9. q : Point
10. r : Point
11. a \# b
12. c \# b
13. x \# y
14. z \# y
15. p \# q
16. r \# q
17. a \# b
18. b \# c
19. x \# y
20. y \# z
21. a1 : Point
22. c1 : Point
23. x1 : Point
24. z1 : Point
25. B(baa1)
26. B(bcc1)
27. B(yxx1)
28. B(yzz1)
29. ba1 \mcong{} yx1
30. bc1 \mcong{} yz1
31. a1c1 \mcong{} x1z1
32. x \# y
33. y \# z
34. p \# q
35. q \# r
36. a' : Point
37. c' : Point
38. x' : Point
39. z' : Point
40. B(yxa')
41. B(yzc')
42. B(qpx')
43. B(qrz')
44. ya' \mcong{} qx'
45. yc' \mcong{} qz'
46. a'c' \mcong{} x'z'
47. A : Point
48. B(ba1A)
49. a1A \mcong{} qx'
50. X : Point
51. B(qx'X)
52. x'X \mcong{} ba1
53. C : Point
54. B(bc1C)
55. c1C \mcong{} qz'
56. Z : Point
57. B(qz'Z)
58. z'Z \mcong{} bc1
59. B(baA)
60. B(bcC)
61. B(qpX)
62. B(qrZ)
63. bA \mcong{} qX
64. bC \mcong{} qZ
65. B(qpX)
66. B(qrZ)
67. bA \mcong{} qX
68. bC \mcong{} qZ
69. X0 : Point
70. Z0 : Point
71. B(bX0a1)
72. B(bZ0c1)
73. yx \mcong{} bX0
74. xx1 \mcong{} X0a1
75. yz \mcong{} bZ0
76. zz1 \mcong{} Z0c1
77. X0Z0 \mcong{} xz
78. \mexists{}X1,Z1:Point. ((B(qX1x') \mwedge{} B(qZ1z')) \mwedge{} yx \mcong{} qX1 \mwedge{} (xa' \mcong{} X1x' \mwedge{} yz \mcong{} qZ1) \mwedge{} zc' \mcong{} Z1z')
\mvdash{} AC \mcong{} XZ
By
Latex:
(ExRepD
THEN (Assert X1Z1 \mcong{} xz BY
(InstLemma `geo-inner-five-segment` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}Z1\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{};\mkleeneopen{}X1\mkleeneclose{}]\mcdot{}
THEN Auto
))
THEN InstLemma `geo-inner-five-segment` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}X1\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{}]\mcdot{}
THEN Auto)
Home
Index