Step
*
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) ∧ a1A ≅ qx'
49. X : Point
50. B(qx'X) ∧ x'X ≅ ba1
51. C : Point
52. B(bc1C) ∧ c1C ≅ qz'
53. Z : Point
54. B(qz'Z) ∧ z'Z ≅ bc1
⊢ ∃a',c',x',z':Point. (B(baa') ∧ B(bcc') ∧ B(qpx') ∧ B(qrz') ∧ ba' ≅ qx' ∧ bc' ≅ qz' ∧ a'c' ≅ x'z')
BY
{ ((InstConcl [⌜A⌝;⌜C⌝;⌜X⌝;⌜Z⌝]⋅ THEN Auto)
THEN (Assert B(qpX) BY
(InstLemma `geo-between-exchange4` [⌜e⌝;⌜q⌝;⌜p⌝;⌜x'⌝;⌜X⌝]⋅ THEN Auto))
THEN (Assert B(qrZ) BY
(InstLemma `geo-between-exchange4` [⌜e⌝;⌜q⌝;⌜r⌝;⌜z'⌝;⌜Z⌝]⋅ THEN Auto))
THEN (Assert ⌜bA ≅ qX⌝⋅ THEN Auto)
THEN Assert ⌜bC ≅ qZ⌝⋅
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
⊢ 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) \mwedge{} a1A \mcong{} qx'
49. X : Point
50. B(qx'X) \mwedge{} x'X \mcong{} ba1
51. C : Point
52. B(bc1C) \mwedge{} c1C \mcong{} qz'
53. Z : Point
54. B(qz'Z) \mwedge{} z'Z \mcong{} bc1
\mvdash{} \mexists{}a',c',x',z':Point. (B(baa') \mwedge{} B(bcc') \mwedge{} B(qpx') \mwedge{} B(qrz') \mwedge{} ba' \mcong{} qx' \mwedge{} bc' \mcong{} qz' \mwedge{} a'c' \mcong{} x'z')
By
Latex:
((InstConcl [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}Z\mkleeneclose{}]\mcdot{} THEN Auto)
THEN (Assert B(qpX) BY
(InstLemma `geo-between-exchange4` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{}]\mcdot{} THEN Auto))
THEN (Assert B(qrZ) BY
(InstLemma `geo-between-exchange4` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{};\mkleeneopen{}Z\mkleeneclose{}]\mcdot{} THEN Auto))
THEN (Assert \mkleeneopen{}bA \mcong{} qX\mkleeneclose{}\mcdot{} THEN Auto)
THEN Assert \mkleeneopen{}bC \mcong{} qZ\mkleeneclose{}\mcdot{}
THEN Auto)
Home
Index