---

Step * 2 1 1 1 of Lemma r2-upper-dimension


1. t2 : ℝ
2. t1 : ℝ
3. t : ℝ
4. a : ℝ^2
5. b : ℝ^2
6. p : ℝ^2
7. q : ℝ^2
8. r : ℝ^2
9. v : ℝ^2
10. v1 : {y:ℝ^2| (b - a⋅y = r0) ∧ (||y|| = r1)} 
11. v + t2*v1 ≠ v + t1*v1
∧ v + t1*v1 ≠ v + t*v1
∧ v + t*v1 ≠ v + t2*v1
∧ (¬v + t2*v1-v + t1*v1-v + t*v1)
∧ (¬v + t1*v1-v + t*v1-v + t2*v1)
∧ (¬v + t*v1-v + t2*v1-v + t1*v1)
⊢ False
BY
{ SplitAndHyps }

1
1. t2 : ℝ
2. t1 : ℝ
3. t : ℝ
4. a : ℝ^2
5. b : ℝ^2
6. p : ℝ^2
7. q : ℝ^2
8. r : ℝ^2
9. v : ℝ^2
10. v1 : {y:ℝ^2| (b - a⋅y = r0) ∧ (||y|| = r1)} 
11. v + t2*v1 ≠ v + t1*v1
12. v + t1*v1 ≠ v + t*v1
13. v + t*v1 ≠ v + t2*v1
14. ¬v + t2*v1-v + t1*v1-v + t*v1
15. ¬v + t1*v1-v + t*v1-v + t2*v1
16. ¬v + t*v1-v + t2*v1-v + t1*v1
⊢ False

---

Latex:

---

Latex:

1.  t2  :  \mBbbR{}
2.  t1  :  \mBbbR{}
3.  t  :  \mBbbR{}
4.  a  :  \mBbbR{}\^{}2
5.  b  :  \mBbbR{}\^{}2
6.  p  :  \mBbbR{}\^{}2
7.  q  :  \mBbbR{}\^{}2
8.  r  :  \mBbbR{}\^{}2
9.  v  :  \mBbbR{}\^{}2
10.  v1  :  \{y:\mBbbR{}\^{}2|  (b  -  a\mcdot{}y  =  r0)  \mwedge{}  (||y||  =  r1)\} 
11.  v  +  t2*v1  \mneq{}  v  +  t1*v1
\mwedge{}  v  +  t1*v1  \mneq{}  v  +  t*v1
\mwedge{}  v  +  t*v1  \mneq{}  v  +  t2*v1
\mwedge{}  (\mneg{}v  +  t2*v1-v  +  t1*v1-v  +  t*v1)
\mwedge{}  (\mneg{}v  +  t1*v1-v  +  t*v1-v  +  t2*v1)
\mwedge{}  (\mneg{}v  +  t*v1-v  +  t2*v1-v  +  t1*v1)
\mvdash{}  False


By

---

Latex:
SplitAndHyps

---

Home Index