---

Step * 1 of Lemma rv-unit_wf

.....set predicate..... 
1. rv : InnerProductSpace
2. x : Point(rv)
3. x # 0
4. r0 < ||x||
⊢ (r1/||x||)*x^2 = r1
BY
{ ((Assert r0 < (||x|| * ||x||) BY EAuto 1) THEN (RWW "rv-ip-mul rv-ip-mul2 rmul-assoc rmul-rdiv" 0 THENA Auto)) }

1
1. rv : InnerProductSpace
2. x : Point(rv)
3. x # 0
4. r0 < ||x||
5. r0 < (||x|| * ||x||)
⊢ ((r1 * r1/||x|| * ||x||) * x^2) = r1

---

Latex:

---

Latex:
.....set  predicate..... 
1.  rv  :  InnerProductSpace
2.  x  :  Point(rv)
3.  x  \#  0
4.  r0  <  ||x||
\mvdash{}  (r1/||x||)*x\^{}2  =  r1


By

---

Latex:
((Assert  r0  <  (||x||  *  ||x||)  BY
                EAuto  1)
  THEN  (RWW  "rv-ip-mul  rv-ip-mul2  rmul-assoc  rmul-rdiv"  0  THENA  Auto)
  )

---

Home Index