---

Step * 1 1 1 1 2 1 1 1 1 of Lemma hp-angle-sum-eq2


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. xyz ≅a x'y'z'
22. p1 : Point
23. p2 : Point
24. d1 : Point
25. f1 : Point
26. abc ≅a ijp1
27. kjp1 ≅a xyz
28. j_p2_p1
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. j'_p'_p
39. out(j' i'd')
40. out(j' k'f')
41. d'-p'-f'
42. a # bc
43. x # yz
44. A : Point
45. d1-j-A
46. jA ≅ OX
47. B : Point
48. f1-j-B
49. jB ≅ OX
50. d'' : Point
51. A-j-d''
52. jd'' ≅ j'd'
53. f'' : Point
54. B-j-f''
55. jf'' ≅ j'f'
56. C : Point
57. p1-j-C
58. jC ≅ OX
59. p'' : Point
60. C_j_p''
61. jp'' ≅ j'p'
62. out(j f''f1)
63. out(j d''d1)
64. out(j d''i)
65. out(j f''k)
66. j'_d'_d'
67. j'_f'_f'
68. j_d''_d''
69. j_f''_f''
70. j'd' ≅ jd''
71. j'f' ≅ jf''
72. p' ≠ j'
73. out(j p''p1)
74. out(j' pp')
75. a' # b'c'
76. d'j'p' ≅a a'b'c'
77. d' # j'p'
78. d''jp'' ≅a abc
79. d'' # jp''
⊢ d'f' ≅ d''f''
BY
{ ((Assert x' # y'z' BY
          (ProveLSepFromCong ⌜x'⌝⌜y'⌝⌜z'⌝⌜x⌝⌜y⌝⌜z⌝⋅ THEN EAuto 1))
   THEN (Assert f'j'p' ≅a x'y'z' BY
               ((InstLemma `out-preserves-angle-cong_1` [⌜e⌝;⌜k'⌝;⌜j'⌝;⌜p⌝;⌜x'⌝;⌜y'⌝;⌜z'⌝;⌜f'⌝;⌜p'⌝;⌜x'⌝;⌜z'⌝]⋅
                 THEN EAuto 1
                 )
                THEN (D 0 THEN Auto)
                THEN EAuto 1))
   THEN (Assert f' # j'p' BY
               (ProveLSepFromCong ⌜f'⌝⌜j'⌝⌜p'⌝⌜x'⌝⌜y'⌝⌜z'⌝⋅ THEN Auto))) }

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. xyz ≅a x'y'z'
22. p1 : Point
23. p2 : Point
24. d1 : Point
25. f1 : Point
26. abc ≅a ijp1
27. kjp1 ≅a xyz
28. j_p2_p1
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. j'_p'_p
39. out(j' i'd')
40. out(j' k'f')
41. d'-p'-f'
42. a # bc
43. x # yz
44. A : Point
45. d1-j-A
46. jA ≅ OX
47. B : Point
48. f1-j-B
49. jB ≅ OX
50. d'' : Point
51. A-j-d''
52. jd'' ≅ j'd'
53. f'' : Point
54. B-j-f''
55. jf'' ≅ j'f'
56. C : Point
57. p1-j-C
58. jC ≅ OX
59. p'' : Point
60. C_j_p''
61. jp'' ≅ j'p'
62. out(j f''f1)
63. out(j d''d1)
64. out(j d''i)
65. out(j f''k)
66. j'_d'_d'
67. j'_f'_f'
68. j_d''_d''
69. j_f''_f''
70. j'd' ≅ jd''
71. j'f' ≅ jf''
72. p' ≠ j'
73. out(j p''p1)
74. out(j' pp')
75. a' # b'c'
76. d'j'p' ≅a a'b'c'
77. d' # j'p'
78. d''jp'' ≅a abc
79. d'' # jp''
80. x' # y'z'
81. f'j'p' ≅a x'y'z'
82. f' # j'p'
⊢ d'f' ≅ d''f''

---

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.  xyz  \mcong{}\msuba{}  x'y'z'
22.  p1  :  Point
23.  p2  :  Point
24.  d1  :  Point
25.  f1  :  Point
26.  abc  \mcong{}\msuba{}  ijp1
27.  kjp1  \mcong{}\msuba{}  xyz
28.  j\_p2\_p1
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.  j'\_p'\_p
39.  out(j'  i'd')
40.  out(j'  k'f')
41.  d'-p'-f'
42.  a  \#  bc
43.  x  \#  yz
44.  A  :  Point
45.  d1-j-A
46.  jA  \mcong{}  OX
47.  B  :  Point
48.  f1-j-B
49.  jB  \mcong{}  OX
50.  d''  :  Point
51.  A-j-d''
52.  jd''  \mcong{}  j'd'
53.  f''  :  Point
54.  B-j-f''
55.  jf''  \mcong{}  j'f'
56.  C  :  Point
57.  p1-j-C
58.  jC  \mcong{}  OX
59.  p''  :  Point
60.  C\_j\_p''
61.  jp''  \mcong{}  j'p'
62.  out(j  f''f1)
63.  out(j  d''d1)
64.  out(j  d''i)
65.  out(j  f''k)
66.  j'\_d'\_d'
67.  j'\_f'\_f'
68.  j\_d''\_d''
69.  j\_f''\_f''
70.  j'd'  \mcong{}  jd''
71.  j'f'  \mcong{}  jf''
72.  p'  \mneq{}  j'
73.  out(j  p''p1)
74.  out(j'  pp')
75.  a'  \#  b'c'
76.  d'j'p'  \mcong{}\msuba{}  a'b'c'
77.  d'  \#  j'p'
78.  d''jp''  \mcong{}\msuba{}  abc
79.  d''  \#  jp''
\mvdash{}  d'f'  \mcong{}  d''f''


By

---

Latex:
((Assert  x'  \#  y'z'  BY
                (ProveLSepFromCong  \mkleeneopen{}x'\mkleeneclose{}\mkleeneopen{}y'\mkleeneclose{}\mkleeneopen{}z'\mkleeneclose{}\mkleeneopen{}x\mkleeneclose{}\mkleeneopen{}y\mkleeneclose{}\mkleeneopen{}z\mkleeneclose{}\mcdot{}  THEN  EAuto  1))
  THEN  (Assert  f'j'p'  \mcong{}\msuba{}  x'y'z'  BY
                          ((InstLemma  `out-preserves-angle-cong\_1`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}k'\mkleeneclose{};\mkleeneopen{}j'\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}y'\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{};\mkleeneopen{}f'\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{};
                              \mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{}]\mcdot{}
                              THEN  EAuto  1
                              )
                            THEN  (D  0  THEN  Auto)
                            THEN  EAuto  1))
  THEN  (Assert  f'  \#  j'p'  BY
                          (ProveLSepFromCong  \mkleeneopen{}f'\mkleeneclose{}\mkleeneopen{}j'\mkleeneclose{}\mkleeneopen{}p'\mkleeneclose{}\mkleeneopen{}x'\mkleeneclose{}\mkleeneopen{}y'\mkleeneclose{}\mkleeneopen{}z'\mkleeneclose{}\mcdot{}  THEN  Auto)))

---

Home Index