---

Step * 2 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 0) * (x 0)) + ((x 1) * (x 1))) = (||x|| * ||x||)
BY
{ (RWO  "-1" 0 THENA Auto) }

1
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||)

---

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  0)  *  (x  0))  +  ((x  1)  *  (x  1)))  =  (||x||  *  ||x||)


By

---

Latex:
(RWO    "-1"  0  THENA  Auto)

---

Home Index