---

Step * 2 1 1 1 1 1 of Lemma r2-perp_wf


1. x : ℝ^2
2. r0 < ||x||
3. r2-perp(x) ∈ ℝ^2
4. x⋅r2-perp(x) = r0
5. (((x 0) * (x 0)) + ((x 1) * (x 1))) = x⋅x
⊢ x⋅x = (||x|| * ||x||)
BY
{ (RepUR ``real-vec-norm`` 0 THEN RWO "rsqrt_squared" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}\^{}2
2.  r0  <  ||x||
3.  r2-perp(x)  \mmember{}  \mBbbR{}\^{}2
4.  x\mcdot{}r2-perp(x)  =  r0
5.  (((x  0)  *  (x  0))  +  ((x  1)  *  (x  1)))  =  x\mcdot{}x
\mvdash{}  x\mcdot{}x  =  (||x||  *  ||x||)


By

---

Latex:
(RepUR  ``real-vec-norm``  0  THEN  RWO  "rsqrt\_squared"  0  THEN  Auto)

---

Home Index