Step * 1 1 1 1 1 1 1 3 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. a1 ≡ b
⊢ a'@0c'@0 ≅ x1z'
BY
((Assert False BY ((Lemmaize [-1;39;52] THEN Auto) THEN EliminatePoint (-1) THEN Auto)) THEN Auto) }


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.  a1  \mequiv{}  b
\mvdash{}  a'@0c'@0  \mcong{}  x1z'


By


Latex:
((Assert  False  BY  ((Lemmaize  [-1;39;52]  THEN  Auto)  THEN  EliminatePoint  (-1)  THEN  Auto))  THEN  Auto)




Home Index