---

Step * 1 2 1 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
⊢ AC ≅ XZ
BY
{ (Assert ∃X0,Z0:Point. ((B(bX0a1) ∧ B(bZ0c1)) ∧ yx ≅ bX0 ∧ (xx1 ≅ X0a1 ∧ yz ≅ bZ0) ∧ zz1 ≅ Z0c1) BY
         ((InstLemma `geo-congruent-between-exists` [⌜e⌝;⌜y⌝;⌜x⌝;⌜x1⌝;⌜b⌝;⌜a1⌝]⋅ THENA Auto)
          THEN (InstLemma `geo-congruent-between-exists` [⌜e⌝;⌜y⌝;⌜z⌝;⌜z1⌝;⌜b⌝;⌜c1⌝]⋅ THENA Auto)
          THEN (ExRepD THEN RenameVar `P0' 69 THEN RenameVar `R0' 73)
          THEN InstConcl [⌜P0⌝;⌜R0⌝]⋅
          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,Z0:Point. ((B(bX0a1) ∧ B(bZ0c1)) ∧ yx ≅ bX0 ∧ (xx1 ≅ X0a1 ∧ yz ≅ bZ0) ∧ zz1 ≅ Z0c1)
⊢ 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
\mvdash{}  AC  \mcong{}  XZ


By

---

Latex:
(Assert  \mexists{}X0,Z0:Point.  ((B(bX0a1)  \mwedge{}  B(bZ0c1))  \mwedge{}  yx  \mcong{}  bX0  \mwedge{}  (xx1  \mcong{}  X0a1  \mwedge{}  yz  \mcong{}  bZ0)  \mwedge{}  zz1  \mcong{}  Z0c1)  BY
              ((InstLemma  `geo-congruent-between-exists`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  (InstLemma  `geo-congruent-between-exists`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}z1\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c1\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  (ExRepD  THEN  RenameVar  `P0'  69  THEN  RenameVar  `R0'  73)
                THEN  InstConcl  [\mkleeneopen{}P0\mkleeneclose{};\mkleeneopen{}R0\mkleeneclose{}]\mcdot{}
                THEN  Auto))

---

Home Index