Step
*
1
of Lemma
not-not-inner-pasch
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. p : Point
6. a_p_c
7. q : Point
8. b_q_c
⊢ ¬¬(∃x:Point. (p_x_b ∧ q_x_a))
BY
{ ((InstLemma `eu-colinear-cases` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝]⋅ THENA Auto) THEN BHyp -1 THEN ((D 0 THENA Auto) ORELSE Auto)) }
1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. p : Point
6. a_p_c
7. q : Point
8. b_q_c
9. ∀X:ℙ
(Stable{X}
⇒ (((¬(a = b ∈ Point)) ∧ (c = a ∈ Point))
⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ (c = b ∈ Point))
⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ c-a-b)
⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ a-c-b)
⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ a-b-c)
⇒ X)
⇒ ((¬Colinear(a;b;c))
⇒ X)
⇒ X)
10. ¬¬¬¬(∃x:Point. (p_x_b ∧ q_x_a))
⊢ ¬¬(∃x:Point. (p_x_b ∧ q_x_a))
2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. p : Point
6. a_p_c
7. q : Point
8. b_q_c
9. ∀X:ℙ
(Stable{X}
⇒ (((¬(a = b ∈ Point)) ∧ (c = a ∈ Point))
⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ (c = b ∈ Point))
⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ c-a-b)
⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ a-c-b)
⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ a-b-c)
⇒ X)
⇒ ((¬Colinear(a;b;c))
⇒ X)
⇒ X)
10. (¬(a = b ∈ Point)) ∧ (c = a ∈ Point)
⊢ ¬¬(∃x:Point. (p_x_b ∧ q_x_a))
3
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. p : Point
6. a_p_c
7. q : Point
8. b_q_c
9. ∀X:ℙ
(Stable{X}
⇒ (((¬(a = b ∈ Point)) ∧ (c = a ∈ Point))
⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ (c = b ∈ Point))
⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ c-a-b)
⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ a-c-b)
⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ a-b-c)
⇒ X)
⇒ ((¬Colinear(a;b;c))
⇒ X)
⇒ X)
10. (¬(a = b ∈ Point)) ∧ (c = b ∈ Point)
⊢ ¬¬(∃x:Point. (p_x_b ∧ q_x_a))
4
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. p : Point
6. a_p_c
7. q : Point
8. b_q_c
9. ∀X:ℙ
(Stable{X}
⇒ (((¬(a = b ∈ Point)) ∧ (c = a ∈ Point))
⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ (c = b ∈ Point))
⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ c-a-b)
⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ a-c-b)
⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ a-b-c)
⇒ X)
⇒ ((¬Colinear(a;b;c))
⇒ X)
⇒ X)
10. (¬(a = b ∈ Point)) ∧ c-a-b
⊢ ¬¬(∃x:Point. (p_x_b ∧ q_x_a))
5
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. p : Point
6. a_p_c
7. q : Point
8. b_q_c
9. ∀X:ℙ
(Stable{X}
⇒ (((¬(a = b ∈ Point)) ∧ (c = a ∈ Point))
⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ (c = b ∈ Point))
⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ c-a-b)
⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ a-c-b)
⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ a-b-c)
⇒ X)
⇒ ((¬Colinear(a;b;c))
⇒ X)
⇒ X)
10. (¬(a = b ∈ Point)) ∧ a-c-b
⊢ ¬¬(∃x:Point. (p_x_b ∧ q_x_a))
6
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. p : Point
6. a_p_c
7. q : Point
8. b_q_c
9. ∀X:ℙ
(Stable{X}
⇒ (((¬(a = b ∈ Point)) ∧ (c = a ∈ Point))
⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ (c = b ∈ Point))
⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ c-a-b)
⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ a-c-b)
⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ a-b-c)
⇒ X)
⇒ ((¬Colinear(a;b;c))
⇒ X)
⇒ X)
10. (¬(a = b ∈ Point)) ∧ a-b-c
⊢ ¬¬(∃x:Point. (p_x_b ∧ q_x_a))
7
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. p : Point
6. a_p_c
7. q : Point
8. b_q_c
9. ∀X:ℙ
(Stable{X}
⇒ (((¬(a = b ∈ Point)) ∧ (c = a ∈ Point))
⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ (c = b ∈ Point))
⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ c-a-b)
⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ a-c-b)
⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ a-b-c)
⇒ X)
⇒ ((¬Colinear(a;b;c))
⇒ X)
⇒ X)
10. ¬Colinear(a;b;c)
⊢ ¬¬(∃x:Point. (p_x_b ∧ q_x_a))
Latex:
Latex:
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. p : Point
6. a\_p\_c
7. q : Point
8. b\_q\_c
\mvdash{} \mneg{}\mneg{}(\mexists{}x:Point. (p\_x\_b \mwedge{} q\_x\_a))
By
Latex:
((InstLemma `eu-colinear-cases` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{} THENA Auto)
THEN BHyp -1
THEN ((D 0 THENA Auto) ORELSE Auto))
Home
Index