Step * 1 1 1 1 1 1 1 2 of Lemma opp-side_half-plane-angle-congruence


1. EuclideanPlane
2. Point
3. Point
4. b' Point
5. p' Point
6. Point
7. Point
8. a' Point
9. c' Point
10. leftof bp
11. leftof pb
12. a' leftof b'p'
13. c' leftof p'b'
14. abp ≅a a'b'p'
15. pbc ≅a p'b'c'
16. b
17. p
18. a' b'
19. b' p'
20. a'@0 Point
21. c1 Point
22. x1 Point
23. z1 Point
24. B(baa'@0)
25. B(bpc1)
26. B(b'a'x1)
27. B(b'p'z1)
28. ba'@0 ≅ b'x1
29. bc1 ≅ b'z1
30. a'@0c1 ≅ x1z1
31. b
32. c
33. p' b'
34. b' c'
35. a1 Point
36. c'@0 Point
37. x' Point
38. z' Point
39. B(bpa1)
40. B(bcc'@0)
41. B(b'p'x')
42. B(b'c'z')
43. ba1 ≅ b'x'
44. bc'@0 ≅ b'z'
45. a1c'@0 ≅ x'z'
46. B(baa'@0)
47. B(bcc'@0)
48. B(b'a'x1)
49. B(b'c'z')
50. ba'@0 ≅ b'x1
51. bc'@0 ≅ b'z'
52. a'@0 leftof bp
53. c'@0 leftof pb
54. x1 leftof b'p'
55. z' leftof p'b'
56. a'@0ba1 ≅a x1b'x'
57. a1bc'@0 ≅a x'b'z'
58. x' z'
59. z' leftof x'b'
60. x1 x'
61. c'@0 pb  ((∀x:Point. (Colinear(x;p;b)  c'@0 x)) ∧ b)
62. c'@0 pb  (∀x:Point. (Colinear(x;p;b)  c'@0 x)) ∧ b
63. a'@0 bp  ((∀x:Point. (Colinear(x;b;p)  a'@0 x)) ∧ p)
64. a'@0 bp  (∀x:Point. (Colinear(x;b;p)  a'@0 x)) ∧ p
65. Point
66. Colinear(b;p;x)
67. B(a'@0xc'@0)
68. Colinear(b;x;a1)
69. a'@0a1 ≅ x1x'
70. x ≡ a1
⊢ a'@0c'@0 ≅ x1z'
BY
(DupHyp (-4) THEN (RWO  "-2" (-1) THENA Auto)) }

1
1. EuclideanPlane
2. Point
3. Point
4. b' Point
5. p' Point
6. Point
7. Point
8. a' Point
9. c' Point
10. leftof bp
11. leftof pb
12. a' leftof b'p'
13. c' leftof p'b'
14. abp ≅a a'b'p'
15. pbc ≅a p'b'c'
16. b
17. p
18. a' b'
19. b' p'
20. a'@0 Point
21. c1 Point
22. x1 Point
23. z1 Point
24. B(baa'@0)
25. B(bpc1)
26. B(b'a'x1)
27. B(b'p'z1)
28. ba'@0 ≅ b'x1
29. bc1 ≅ b'z1
30. a'@0c1 ≅ x1z1
31. b
32. c
33. p' b'
34. b' c'
35. a1 Point
36. c'@0 Point
37. x' Point
38. z' Point
39. B(bpa1)
40. B(bcc'@0)
41. B(b'p'x')
42. B(b'c'z')
43. ba1 ≅ b'x'
44. bc'@0 ≅ b'z'
45. a1c'@0 ≅ x'z'
46. B(baa'@0)
47. B(bcc'@0)
48. B(b'a'x1)
49. B(b'c'z')
50. ba'@0 ≅ b'x1
51. bc'@0 ≅ b'z'
52. a'@0 leftof bp
53. c'@0 leftof pb
54. x1 leftof b'p'
55. z' leftof p'b'
56. a'@0ba1 ≅a x1b'x'
57. a1bc'@0 ≅a x'b'z'
58. x' z'
59. z' leftof x'b'
60. x1 x'
61. c'@0 pb  ((∀x:Point. (Colinear(x;p;b)  c'@0 x)) ∧ b)
62. c'@0 pb  (∀x:Point. (Colinear(x;p;b)  c'@0 x)) ∧ b
63. a'@0 bp  ((∀x:Point. (Colinear(x;b;p)  a'@0 x)) ∧ p)
64. a'@0 bp  (∀x:Point. (Colinear(x;b;p)  a'@0 x)) ∧ p
65. Point
66. Colinear(b;p;x)
67. B(a'@0xc'@0)
68. Colinear(b;x;a1)
69. a'@0a1 ≅ x1x'
70. x ≡ a1
71. B(a'@0a1c'@0)
⊢ a'@0c'@0 ≅ x1z'


Latex:


Latex:

1.  e  :  EuclideanPlane
2.  b  :  Point
3.  p  :  Point
4.  b'  :  Point
5.  p'  :  Point
6.  a  :  Point
7.  c  :  Point
8.  a'  :  Point
9.  c'  :  Point
10.  a  leftof  bp
11.  c  leftof  pb
12.  a'  leftof  b'p'
13.  c'  leftof  p'b'
14.  abp  \mcong{}\msuba{}  a'b'p'
15.  pbc  \mcong{}\msuba{}  p'b'c'
16.  a  \#  b
17.  b  \#  p
18.  a'  \#  b'
19.  b'  \#  p'
20.  a'@0  :  Point
21.  c1  :  Point
22.  x1  :  Point
23.  z1  :  Point
24.  B(baa'@0)
25.  B(bpc1)
26.  B(b'a'x1)
27.  B(b'p'z1)
28.  ba'@0  \mcong{}  b'x1
29.  bc1  \mcong{}  b'z1
30.  a'@0c1  \mcong{}  x1z1
31.  p  \#  b
32.  b  \#  c
33.  p'  \#  b'
34.  b'  \#  c'
35.  a1  :  Point
36.  c'@0  :  Point
37.  x'  :  Point
38.  z'  :  Point
39.  B(bpa1)
40.  B(bcc'@0)
41.  B(b'p'x')
42.  B(b'c'z')
43.  ba1  \mcong{}  b'x'
44.  bc'@0  \mcong{}  b'z'
45.  a1c'@0  \mcong{}  x'z'
46.  B(baa'@0)
47.  B(bcc'@0)
48.  B(b'a'x1)
49.  B(b'c'z')
50.  ba'@0  \mcong{}  b'x1
51.  bc'@0  \mcong{}  b'z'
52.  a'@0  leftof  bp
53.  c'@0  leftof  pb
54.  x1  leftof  b'p'
55.  z'  leftof  p'b'
56.  a'@0ba1  \mcong{}\msuba{}  x1b'x'
57.  a1bc'@0  \mcong{}\msuba{}  x'b'z'
58.  x'  \#  z'
59.  z'  leftof  x'b'
60.  x1  \#  x'
61.  c'@0  \#  pb  {}\mRightarrow{}  ((\mforall{}x:Point.  (Colinear(x;p;b)  {}\mRightarrow{}  c'@0  \#  x))  \mwedge{}  p  \#  b)
62.  c'@0  \#  pb  \mLeftarrow{}{}  (\mforall{}x:Point.  (Colinear(x;p;b)  {}\mRightarrow{}  c'@0  \#  x))  \mwedge{}  p  \#  b
63.  a'@0  \#  bp  {}\mRightarrow{}  ((\mforall{}x:Point.  (Colinear(x;b;p)  {}\mRightarrow{}  a'@0  \#  x))  \mwedge{}  b  \#  p)
64.  a'@0  \#  bp  \mLeftarrow{}{}  (\mforall{}x:Point.  (Colinear(x;b;p)  {}\mRightarrow{}  a'@0  \#  x))  \mwedge{}  b  \#  p
65.  x  :  Point
66.  Colinear(b;p;x)
67.  B(a'@0xc'@0)
68.  Colinear(b;x;a1)
69.  a'@0a1  \mcong{}  x1x'
70.  x  \mequiv{}  a1
\mvdash{}  a'@0c'@0  \mcong{}  x1z'


By


Latex:
(DupHyp  (-4)  THEN  (RWO    "-2"  (-1)  THENA  Auto))




Home Index