---

Step * 1 1 1 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 1)/||x||)
9. i = 0 ∈ ℤ
10. (-(x 1)/||x||) ≠ r0
11. i1 : ℤ
12. i1 = 0 ∈ ℤ
⊢ (y 0) = ((y 0/(-(x 1)/||x||)) * (-(x 1)/||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  1)/||x||)
9.  i  =  0
10.  (-(x  1)/||x||)  \mneq{}  r0
11.  i1  :  \mBbbZ{}
12.  i1  =  0
\mvdash{}  (y  0)  =  ((y  0/(-(x  1)/||x||))  *  (-(x  1)/||x||))


By

---

Latex:
Auto

---

Home Index