---

Step * 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. abc ≅a xyz
18. xyz ≅a pqr
⊢ abc ≅a pqr
BY
{ ((((Unfold `geo-cong-angle` 0 THEN D 18 THEN D 17) THEN ExRepD)
    THEN ((gProlong ⌜b⌝⌜a1⌝`A'⌜q⌝⌜x'⌝⋅ THENA Auto) THEN (gProlong ⌜q⌝⌜x'⌝ `X' ⌜b⌝⌜a1⌝⋅ THENA Auto))
    THEN (gProlong ⌜b⌝⌜c1⌝`C'⌜q⌝⌜z'⌝⋅ THENA Auto)
    THEN (gProlong ⌜q⌝⌜z'⌝`Z'⌜b⌝⌜c1⌝⋅ THENA Auto))
   THEN D 0
   ) }

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) ∧ 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 # b ∧ b # c) ∧ p # q) ∧ q # r

2
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')

---

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.  abc  \mcong{}\msuba{}  xyz
18.  xyz  \mcong{}\msuba{}  pqr
\mvdash{}  abc  \mcong{}\msuba{}  pqr


By

---

Latex:
((((Unfold  `geo-cong-angle`  0  THEN  D  18  THEN  D  17)  THEN  ExRepD)
    THEN  ((gProlong  \mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}a1\mkleeneclose{}`A'\mkleeneopen{}q\mkleeneclose{}\mkleeneopen{}x'\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  (gProlong  \mkleeneopen{}q\mkleeneclose{}\mkleeneopen{}x'\mkleeneclose{}  `X'  \mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}a1\mkleeneclose{}\mcdot{}  THENA  Auto))
    THEN  (gProlong  \mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}c1\mkleeneclose{}`C'\mkleeneopen{}q\mkleeneclose{}\mkleeneopen{}z'\mkleeneclose{}\mcdot{}  THENA  Auto)
    THEN  (gProlong  \mkleeneopen{}q\mkleeneclose{}\mkleeneopen{}z'\mkleeneclose{}`Z'\mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}c1\mkleeneclose{}\mcdot{}  THENA  Auto))
  THEN  D  0
  )

---

Home Index