---

Step * 2 1 1 of Lemma r2-perp_wf


1. x : ℝ^2
2. r0 < ||x||
3. r2-perp(x) ∈ ℝ^2
4. x⋅r2-perp(x) = r0
⊢ (((x 0) * (x 0/||x||)) + -((x 1) * (-(x 1)/||x||))) = ||x||
BY
{ (nRMul ⌜||x||⌝ 0⋅ THEN Auto) }

1
1. x : ℝ^2
2. r0 < ||x||
3. r2-perp(x) ∈ ℝ^2
4. x⋅r2-perp(x) = r0
⊢ (((x 0) * (x 0)) + ((x 1) * (x 1))) = (||x|| * ||x||)

---

Latex:

---

Latex:

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


By

---

Latex:
(nRMul  \mkleeneopen{}||x||\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index