---

Step * 2 1 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
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
BY
{ ((DSetVars THEN (Assert r0 < ||v1|| BY (Auto THEN RWO "-7" 0 THEN Auto)))
   THEN ∀h:hyp. ((RWO  "rv-between-translation" h THENM RWO  "rv-between-vec-mul" h) THENA Auto) 
   ) }

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 : ℝ^2
11. (b - a⋅v1 = r0) ∧ (||v1|| = r1)
12. v + t2*v1 ≠ v + t1*v1
13. v + t1*v1 ≠ v + t*v1
14. v + t*v1 ≠ v + t2*v1
15. ¬(((t2 < t1) ∧ (t1 < t)) ∨ ((t < t1) ∧ (t1 < t2)))
16. ¬(((t1 < t) ∧ (t < t2)) ∨ ((t2 < t) ∧ (t < t1)))
17. ¬(((t < t2) ∧ (t2 < t1)) ∨ ((t1 < t2) ∧ (t2 < t)))
18. r0 < ||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
12.  v  +  t1*v1  \mneq{}  v  +  t*v1
13.  v  +  t*v1  \mneq{}  v  +  t2*v1
14.  \mneg{}v  +  t2*v1-v  +  t1*v1-v  +  t*v1
15.  \mneg{}v  +  t1*v1-v  +  t*v1-v  +  t2*v1
16.  \mneg{}v  +  t*v1-v  +  t2*v1-v  +  t1*v1
\mvdash{}  False


By

---

Latex:
((DSetVars  THEN  (Assert  r0  <  ||v1||  BY  (Auto  THEN  RWO  "-7"  0  THEN  Auto)))
  THEN  \mforall{}h:hyp.  ((RWO    "rv-between-translation"  h  THENM  RWO    "rv-between-vec-mul"  h)  THENA  Auto) 
  )

---

Home Index