---

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


1. x : ℝ^2
2. r0 < ||x||
3. y : ℝ^2
4. y⋅x = r0
5. ||r2-perp(x)|| = r1
6. r0 < ||r2-perp(x)||
7. i : ℤ
8. r0 ≠ (x 0/||x||)
9. i = 1 ∈ ℤ
10. (x 0/||x||) ≠ r0
11. i1 : ℤ
12. i1 = 1 ∈ ℤ
⊢ (y 1) = ((y 1/(x 0/||x||)) * (x 0/||x||))
BY
{ Auto }

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}\^{}2
2.  r0  <  ||x||
3.  y  :  \mBbbR{}\^{}2
4.  y\mcdot{}x  =  r0
5.  ||r2-perp(x)||  =  r1
6.  r0  <  ||r2-perp(x)||
7.  i  :  \mBbbZ{}
8.  r0  \mneq{}  (x  0/||x||)
9.  i  =  1
10.  (x  0/||x||)  \mneq{}  r0
11.  i1  :  \mBbbZ{}
12.  i1  =  1
\mvdash{}  (y  1)  =  ((y  1/(x  0/||x||))  *  (x  0/||x||))


By

---

Latex:
Auto

---

Home Index