Step
*
1
1
1
1
1
1
1
1
of Lemma
opp-side_half-plane-angle-congruence
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 ≅a a'b'p'
15. pbc ≅a 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 ≅ b'x1
29. bc1 ≅ b'z1
30. a'@0c1 ≅ 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 ≅ 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)) ∧ p # b)
62. c'@0 # pb ⇐ (∀x:Point. (Colinear(x;p;b) ⇒ c'@0 # x)) ∧ p # b
63. a'@0 # bp ⇒ ((∀x:Point. (Colinear(x;b;p) ⇒ a'@0 # x)) ∧ b # p)
64. a'@0 # bp ⇐ (∀x:Point. (Colinear(x;b;p) ⇒ a'@0 # x)) ∧ b # p
65. x : Point
66. Colinear(b;p;x)
67. B(a'@0xc'@0)
68. Colinear(b;x;a1)
69. a'@0a1 ≅ x1x'
70. b ≡ x
⊢ a'@0c'@0 ≅ x1z'
BY
{ (((EliminatePoint (-1) THEN Auto)
THEN (Assert x' # z' BY
((InstLemma `lsep-iff-all-sep` [⌜e⌝;⌜z'⌝;⌜p'⌝;⌜b'⌝]⋅ THENA Auto)
THEN ((D -1 THEN D -2) THENA (Unfold `geo-lsep` 0 THEN Auto))
THEN D -1
THEN InstHyp [⌜x'⌝] (-2)⋅
THEN Auto))
THEN (gProperProlong ⌜x1⌝⌜b'⌝`Z'⌜b'⌝⌜z'⌝⋅ THEN Auto)
THEN ExRepD)
THEN (InstLemma `Euclid-Prop7` [⌜e⌝;⌜x'⌝;⌜b'⌝;⌜z'⌝;⌜Z⌝]⋅ THENA Auto)
) }
1
.....wf.....
1. e : EuclideanPlane
2. x : Point
3. b : Point
4. p : Point
5. b' : Point
6. p' : Point
7. a : Point
8. c : Point
9. a' : Point
10. c' : Point
11. a leftof xp
12. c leftof px
13. a' leftof b'p'
14. c' leftof p'b'
15. axp ≅a a'b'p'
16. pxc ≅a p'b'c'
17. a # x
18. x # p
19. a' # b'
20. b' # p'
21. a'@0 : Point
22. c1 : Point
23. x1 : Point
24. z1 : Point
25. B(xaa'@0)
26. B(xpc1)
27. B(b'a'x1)
28. B(b'p'z1)
29. xa'@0 ≅ b'x1
30. xc1 ≅ b'z1
31. a'@0c1 ≅ x1z1
32. p # x
33. x # c
34. p' # b'
35. b' # c'
36. a1 : Point
37. c'@0 : Point
38. x' : Point
39. z' : Point
40. B(xpa1)
41. B(xcc'@0)
42. B(b'p'x')
43. B(b'c'z')
44. xa1 ≅ b'x'
45. xc'@0 ≅ b'z'
46. a1c'@0 ≅ x'z'
47. B(xaa'@0)
48. B(xcc'@0)
49. B(b'a'x1)
50. B(b'c'z')
51. xa'@0 ≅ b'x1
52. xc'@0 ≅ b'z'
53. a'@0 leftof xp
54. c'@0 leftof px
55. x1 leftof b'p'
56. z' leftof p'b'
57. a'@0xa1 ≅a x1b'x'
58. a1xc'@0 ≅a x'b'z'
59. x' # z'
60. z' leftof x'b'
61. x1 # x'
62. c'@0 # px ⇒ ((∀x:Point. (Colinear(x;p;b) ⇒ c'@0 # x)) ∧ p # x)
63. c'@0 # px ⇐ (∀x:Point. (Colinear(x;p;b) ⇒ c'@0 # x)) ∧ p # x
64. a'@0 # xp ⇒ ((∀x:Point. (Colinear(x;b;p) ⇒ a'@0 # x)) ∧ x # p)
65. a'@0 # xp ⇐ (∀x:Point. (Colinear(x;b;p) ⇒ a'@0 # x)) ∧ x # p
66. Colinear(x;p;x)
67. B(a'@0xc'@0)
68. Colinear(x;x;a1)
69. a'@0a1 ≅ x1x'
70. b ≡ x
71. x' # z'
72. Z : Point
73. x1-b'-Z
74. b'Z ≅ b'z'
⊢ Z ∈ {p:Point| p leftof x'b'}
2
.....antecedent.....
1. e : EuclideanPlane
2. x : Point
3. b : Point
4. p : Point
5. b' : Point
6. p' : Point
7. a : Point
8. c : Point
9. a' : Point
10. c' : Point
11. a leftof xp
12. c leftof px
13. a' leftof b'p'
14. c' leftof p'b'
15. axp ≅a a'b'p'
16. pxc ≅a p'b'c'
17. a # x
18. x # p
19. a' # b'
20. b' # p'
21. a'@0 : Point
22. c1 : Point
23. x1 : Point
24. z1 : Point
25. B(xaa'@0)
26. B(xpc1)
27. B(b'a'x1)
28. B(b'p'z1)
29. xa'@0 ≅ b'x1
30. xc1 ≅ b'z1
31. a'@0c1 ≅ x1z1
32. p # x
33. x # c
34. p' # b'
35. b' # c'
36. a1 : Point
37. c'@0 : Point
38. x' : Point
39. z' : Point
40. B(xpa1)
41. B(xcc'@0)
42. B(b'p'x')
43. B(b'c'z')
44. xa1 ≅ b'x'
45. xc'@0 ≅ b'z'
46. a1c'@0 ≅ x'z'
47. B(xaa'@0)
48. B(xcc'@0)
49. B(b'a'x1)
50. B(b'c'z')
51. xa'@0 ≅ b'x1
52. xc'@0 ≅ b'z'
53. a'@0 leftof xp
54. c'@0 leftof px
55. x1 leftof b'p'
56. z' leftof p'b'
57. a'@0xa1 ≅a x1b'x'
58. a1xc'@0 ≅a x'b'z'
59. x' # z'
60. z' leftof x'b'
61. x1 # x'
62. c'@0 # px ⇒ ((∀x:Point. (Colinear(x;p;b) ⇒ c'@0 # x)) ∧ p # x)
63. c'@0 # px ⇐ (∀x:Point. (Colinear(x;p;b) ⇒ c'@0 # x)) ∧ p # x
64. a'@0 # xp ⇒ ((∀x:Point. (Colinear(x;b;p) ⇒ a'@0 # x)) ∧ x # p)
65. a'@0 # xp ⇐ (∀x:Point. (Colinear(x;b;p) ⇒ a'@0 # x)) ∧ x # p
66. Colinear(x;p;x)
67. B(a'@0xc'@0)
68. Colinear(x;x;a1)
69. a'@0a1 ≅ x1x'
70. b ≡ x
71. x' # z'
72. Z : Point
73. x1-b'-Z
74. b'Z ≅ b'z'
⊢ x'z' ≅ x'Z
3
1. e : EuclideanPlane
2. x : Point
3. b : Point
4. p : Point
5. b' : Point
6. p' : Point
7. a : Point
8. c : Point
9. a' : Point
10. c' : Point
11. a leftof xp
12. c leftof px
13. a' leftof b'p'
14. c' leftof p'b'
15. axp ≅a a'b'p'
16. pxc ≅a p'b'c'
17. a # x
18. x # p
19. a' # b'
20. b' # p'
21. a'@0 : Point
22. c1 : Point
23. x1 : Point
24. z1 : Point
25. B(xaa'@0)
26. B(xpc1)
27. B(b'a'x1)
28. B(b'p'z1)
29. xa'@0 ≅ b'x1
30. xc1 ≅ b'z1
31. a'@0c1 ≅ x1z1
32. p # x
33. x # c
34. p' # b'
35. b' # c'
36. a1 : Point
37. c'@0 : Point
38. x' : Point
39. z' : Point
40. B(xpa1)
41. B(xcc'@0)
42. B(b'p'x')
43. B(b'c'z')
44. xa1 ≅ b'x'
45. xc'@0 ≅ b'z'
46. a1c'@0 ≅ x'z'
47. B(xaa'@0)
48. B(xcc'@0)
49. B(b'a'x1)
50. B(b'c'z')
51. xa'@0 ≅ b'x1
52. xc'@0 ≅ b'z'
53. a'@0 leftof xp
54. c'@0 leftof px
55. x1 leftof b'p'
56. z' leftof p'b'
57. a'@0xa1 ≅a x1b'x'
58. a1xc'@0 ≅a x'b'z'
59. x' # z'
60. z' leftof x'b'
61. x1 # x'
62. c'@0 # px ⇒ ((∀x:Point. (Colinear(x;p;b) ⇒ c'@0 # x)) ∧ p # x)
63. c'@0 # px ⇐ (∀x:Point. (Colinear(x;p;b) ⇒ c'@0 # x)) ∧ p # x
64. a'@0 # xp ⇒ ((∀x:Point. (Colinear(x;b;p) ⇒ a'@0 # x)) ∧ x # p)
65. a'@0 # xp ⇐ (∀x:Point. (Colinear(x;b;p) ⇒ a'@0 # x)) ∧ x # p
66. Colinear(x;p;x)
67. B(a'@0xc'@0)
68. Colinear(x;x;a1)
69. a'@0a1 ≅ x1x'
70. b ≡ x
71. x' # z'
72. Z : Point
73. x1-b'-Z
74. b'Z ≅ b'z'
75. z' ≡ Z
⊢ 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. b \mequiv{} x
\mvdash{} a'@0c'@0 \mcong{} x1z'
By
Latex:
(((EliminatePoint (-1) THEN Auto)
THEN (Assert x' \# z' BY
((InstLemma `lsep-iff-all-sep` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{}]\mcdot{} THENA Auto)
THEN ((D -1 THEN D -2) THENA (Unfold `geo-lsep` 0 THEN Auto))
THEN D -1
THEN InstHyp [\mkleeneopen{}x'\mkleeneclose{}] (-2)\mcdot{}
THEN Auto))
THEN (gProperProlong \mkleeneopen{}x1\mkleeneclose{}\mkleeneopen{}b'\mkleeneclose{}`Z'\mkleeneopen{}b'\mkleeneclose{}\mkleeneopen{}z'\mkleeneclose{}\mcdot{} THEN Auto)
THEN ExRepD)
THEN (InstLemma `Euclid-Prop7` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{};\mkleeneopen{}Z\mkleeneclose{}]\mcdot{} THENA Auto)
)
Home
Index