---

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


1. rv : InnerProductSpace
2. t : ℝ
3. v : Point
4. r0 < ||v||
5. ((||v|| * ||t*v||) + v ⋅ t*v) = r0
⊢ t ≤ r0
BY
{ (RWW "rv-ip-mul2 rv-norm-mul rv-norm-squared<" (-1)⋅ THENA Auto) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
(RWW  "rv-ip-mul2  rv-norm-mul  rv-norm-squared<"  (-1)\mcdot{}  THENA  Auto)

---

Home Index