Step * 1 2 1 1 1 1 1 of Lemma ip-between-iff


1. rv : InnerProductSpace
2. t : ℝ
3. v : Point
4. r0 < ||v||
5. ((||v|| * |t| * ||v||) + (t * ||v||^2)) = r0
⊢ t ≤ r0
BY
{ nRNorm (-1) }

1
1. rv : InnerProductSpace
2. t : ℝ
3. v : Point
4. r0 < ||v||
5. ((|t| * ||v|| * ||v||) + (||v||^2 * t)) = r0
⊢ t ≤ r0


Latex:


Latex:

1.  rv  :  InnerProductSpace
2.  t  :  \mBbbR{}
3.  v  :  Point
4.  r0  <  ||v||
5.  ((||v||  *  |t|  *  ||v||)  +  (t  *  ||v||\^{}2))  =  r0
\mvdash{}  t  \mleq{}  r0


By


Latex:
nRNorm  (-1)




Home Index