---

Step * 1 1 1 1 1 of Lemma continuous-rinv


1. n : ℕ+
2. k : ℕ+
3. v : ℝ
4. v1 : ℝ
5. v ≠ r0
6. v1 ≠ r0
7. r1 ≤ (r(k) * |v|)
8. r1 ≤ (r(k) * |v1|)
9. |-(v) + v1| ≤ (r1/r((k * k) * n))
⊢ r(n) ≤ (((r(k) * r(k)) * r(n)) * |v| * |v1|)
BY
{ (Assert (r1 * r1) ≤ ((r(k) * |v|) * r(k) * |v1|) BY
         (RWO "-3< " 0 THEN Auto)) }

1
1. n : ℕ+
2. k : ℕ+
3. v : ℝ
4. v1 : ℝ
5. v ≠ r0
6. v1 ≠ r0
7. r1 ≤ (r(k) * |v|)
8. r1 ≤ (r(k) * |v1|)
9. |-(v) + v1| ≤ (r1/r((k * k) * n))
10. (r1 * r1) ≤ ((r(k) * |v|) * r(k) * |v1|)
⊢ r(n) ≤ (((r(k) * r(k)) * r(n)) * |v| * |v1|)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  k  :  \mBbbN{}\msupplus{}
3.  v  :  \mBbbR{}
4.  v1  :  \mBbbR{}
5.  v  \mneq{}  r0
6.  v1  \mneq{}  r0
7.  r1  \mleq{}  (r(k)  *  |v|)
8.  r1  \mleq{}  (r(k)  *  |v1|)
9.  |-(v)  +  v1|  \mleq{}  (r1/r((k  *  k)  *  n))
\mvdash{}  r(n)  \mleq{}  (((r(k)  *  r(k))  *  r(n))  *  |v|  *  |v1|)


By

---

Latex:
(Assert  (r1  *  r1)  \mleq{}  ((r(k)  *  |v|)  *  r(k)  *  |v1|)  BY
              (RWO  "-3<  "  0  THEN  Auto))

---

Home Index