---

Step * 2 1 of Lemma r2-upper-dimension


1. a : ℝ^2
2. b : ℝ^2
3. p : ℝ^2
4. q : ℝ^2
5. r : ℝ^2
6. v : ℝ^2
7. v1 : {y:ℝ^2| (b - a⋅y = r0) ∧ (||y|| = r1)} 
8. ∃t:ℝ. req-vec(2;p;v + t*v1)
9. ∃t:ℝ. req-vec(2;q;v + t*v1)
10. ∃t:ℝ. req-vec(2;r;v + t*v1)
⊢ ¬(p ≠ q ∧ q ≠ r ∧ r ≠ p ∧ (¬p-q-r) ∧ (¬q-r-p) ∧ (¬r-p-q))
BY
{ RepeatFor 3 ((D -1 THEN (RWO "-1" 0 THENA Auto) THEN Thin (-1) THEN PromoteHyp (-1) 1)) }

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)} 
⊢ ¬(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))

---

Latex:

---

Latex:

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


By

---

Latex:
RepeatFor  3  ((D  -1  THEN  (RWO  "-1"  0  THENA  Auto)  THEN  Thin  (-1)  THEN  PromoteHyp  (-1)  1))

---

Home Index