---

Step * of Lemma r2-dot-product-eq-0-iff-perp

∀x:ℝ^2. ((r0 < ||x||) ⇒ (∀y:ℝ^2. (y⋅x = r0 ⇐⇒ ∃t:ℝ. req-vec(2;y;t*r2-perp(x)))))
BY
{ Auto }

1
1. x : ℝ^2
2. r0 < ||x||
3. y : ℝ^2
4. y⋅x = r0
⊢ ∃t:ℝ. req-vec(2;y;t*r2-perp(x))

2
1. x : ℝ^2
2. r0 < ||x||
3. y : ℝ^2
4. ∃t:ℝ. req-vec(2;y;t*r2-perp(x))
⊢ y⋅x = r0

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}\^{}2.  ((r0  <  ||x||)  {}\mRightarrow{}  (\mforall{}y:\mBbbR{}\^{}2.  (y\mcdot{}x  =  r0  \mLeftarrow{}{}\mRightarrow{}  \mexists{}t:\mBbbR{}.  req-vec(2;y;t*r2-perp(x)))))


By

---

Latex:
Auto

---

Home Index