---

Step * 2 1 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 : ℝ^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
BY
{ (ExRepD
   THEN ∀h:hyp. (UnfoldTop `real-vec-sep` h
                 THEN (RWO  "real-vec-dist-translation2" h THENA Auto)
                 THEN (RWO  "real-vec-dist-vec-mul" h THENA Auto)
                 THEN (RWO "12" h THENA Auto)
                 THEN (nRNorm h THENA Auto)
                 THEN (RWO "rabs-positive-iff<" h THENA Auto)
                 THEN D h) 
   THEN nRAdd ⌜t1⌝ (-7)⋅
   THEN nRAdd ⌜t⌝ (-6)⋅
   THEN nRAdd ⌜t2⌝ (-5)⋅
   THEN Try ((D -4 THEN Complete (Auto)))
   THEN Try ((D -3 THEN Complete (Auto)))
   THEN Try ((D -2 THEN Complete (Auto)))) }

---

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


By

---

Latex:
(ExRepD
  THEN  \mforall{}h:hyp.  (UnfoldTop  `real-vec-sep`  h
                              THEN  (RWO    "real-vec-dist-translation2"  h  THENA  Auto)
                              THEN  (RWO    "real-vec-dist-vec-mul"  h  THENA  Auto)
                              THEN  (RWO  "12"  h  THENA  Auto)
                              THEN  (nRNorm  h  THENA  Auto)
                              THEN  (RWO  "rabs-positive-iff<"  h  THENA  Auto)
                              THEN  D  h) 
  THEN  nRAdd  \mkleeneopen{}t1\mkleeneclose{}  (-7)\mcdot{}
  THEN  nRAdd  \mkleeneopen{}t\mkleeneclose{}  (-6)\mcdot{}
  THEN  nRAdd  \mkleeneopen{}t2\mkleeneclose{}  (-5)\mcdot{}
  THEN  Try  ((D  -4  THEN  Complete  (Auto)))
  THEN  Try  ((D  -3  THEN  Complete  (Auto)))
  THEN  Try  ((D  -2  THEN  Complete  (Auto))))

---

Home Index