Proof of Nuprl Lemma : opp-side_half-plane-angle-congruence

Step * 1 1 1 1 1 1 1 6 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. a1-b-x
⊢ a'@0c'@0 ≅ x1z'
BY
{ (((gProperProlong ⌜p'⌝⌜b'⌝`x\'\''⌜b⌝⌜x⌝⋅ THEN Auto) THEN ExRepD)
   THEN (Assert x1 # x'' BY
               ((InstLemma `lsep-iff-all-sep` [⌜e⌝;⌜x1⌝;⌜b'⌝;⌜p'⌝]⋅ THENA Auto)
                THEN ((D -1 THEN D -2) THENA (Unfold `geo-lsep` 0 THEN Auto))
                THEN InstHyp [⌜x''⌝] (-1)⋅
                THEN Auto))
   ) }

1
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. a1-b-x
71. x'' : Point
72. p'-b'-x''
73. b'x'' ≅ bx
74. x1 # x''
⊢ 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. a1-b-x \mvdash{} a'@0c'@0 \mcong{} x1z' By Latex: (((gProperProlong \mkleeneopen{}p'\mkleeneclose{}\mkleeneopen{}b'\mkleeneclose{}`x\mbackslash{}'\mbackslash{}''\mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}x\mkleeneclose{}\mcdot{} THEN Auto) THEN ExRepD) THEN (Assert x1 \# x'' BY ((InstLemma `lsep-iff-all-sep` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{}]\mcdot{} THENA Auto) THEN ((D -1 THEN D -2) THENA (Unfold `geo-lsep` 0 THEN Auto)) THEN InstHyp [\mkleeneopen{}x''\mkleeneclose{}] (-1)\mcdot{} THEN Auto)) ) Home Index