---

Step * 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))
⊢ (r1/r((k * k) * n)) ≤ (|v * v1|/r(n))
BY
{ ((nRMul ⌜r((k * k) * n)⌝ 0⋅ THEN nRMul ⌜r(n)⌝ 0⋅)
   THEN (RWW "rabs-rmul rmul-int<" 0 THENA Auto)
   THEN nRMul ⌜r(k)⌝ (-3)⋅
   THEN nRMul ⌜r(k)⌝ (-2)⋅) }

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))
⊢ 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/r(k))  \mleq{}  |v|
8.  (r1/r(k))  \mleq{}  |v1|
9.  |-(v)  +  v1|  \mleq{}  (r1/r((k  *  k)  *  n))
\mvdash{}  (r1/r((k  *  k)  *  n))  \mleq{}  (|v  *  v1|/r(n))


By

---

Latex:
((nRMul  \mkleeneopen{}r((k  *  k)  *  n)\mkleeneclose{}  0\mcdot{}  THEN  nRMul  \mkleeneopen{}r(n)\mkleeneclose{}  0\mcdot{})
  THEN  (RWW  "rabs-rmul  rmul-int<"  0  THENA  Auto)
  THEN  nRMul  \mkleeneopen{}r(k)\mkleeneclose{}  (-3)\mcdot{}
  THEN  nRMul  \mkleeneopen{}r(k)\mkleeneclose{}  (-2)\mcdot{})

---

Home Index