---

Step * 2 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
⊢ (((x 0) * (x 0)) + ((x 1) * (x 1))) = (||x|| * ||x||)
BY
{ (Assert (((x 0) * (x 0)) + ((x 1) * (x 1))) = x⋅x BY
         (RepUR ``dot-product`` 0
          THEN (RWO "rsum-split-first" 0 THENA Auto)
          THEN Reduce 0
          THEN (RWO "rsum-single" 0 THENA Auto)
          THEN Reduce 0⋅
          THEN 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 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  1)  *  (x  1)))  =  (||x||  *  ||x||)


By

---

Latex:
(Assert  (((x  0)  *  (x  0))  +  ((x  1)  *  (x  1)))  =  x\mcdot{}x  BY
              (RepUR  ``dot-product``  0
                THEN  (RWO  "rsum-split-first"  0  THENA  Auto)
                THEN  Reduce  0
                THEN  (RWO  "rsum-single"  0  THENA  Auto)
                THEN  Reduce  0\mcdot{}
                THEN  Auto))

---

Home Index