---

Step * 1 1 1 1 2 1 of Lemma ip-non-trivial


1. rv : InnerProductSpace
2. x : {x:Point| r0 < ||x||} 
3. y : Point
4. y^2 = r1
5. x ⋅ y = r0
⊢ r0 < ((x^2 - r(2) * r0) + r1)
BY
{ ((Assert r0 ≤ x^2 BY Auto) THEN (RWO "-1<" 0 THENA Auto)) }

1
1. rv : InnerProductSpace
2. x : {x:Point| r0 < ||x||} 
3. y : Point
4. y^2 = r1
5. x ⋅ y = r0
6. r0 ≤ x^2
⊢ r0 < ((r0 - r(2) * r0) + r1)

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  x  :  \{x:Point|  r0  <  ||x||\} 
3.  y  :  Point
4.  y\^{}2  =  r1
5.  x  \mcdot{}  y  =  r0
\mvdash{}  r0  <  ((x\^{}2  -  r(2)  *  r0)  +  r1)


By

---

Latex:
((Assert  r0  \mleq{}  x\^{}2  BY  Auto)  THEN  (RWO  "-1<"  0  THENA  Auto))

---

Home Index