---

Step * 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/v) - (r1/v1)| ≤ (r1/r(n))
BY
{ ((nRMul ⌜|v|⌝ 0⋅ THENA EAuto 1)
   THEN (nRMul ⌜|v1|⌝ 0⋅ THENA EAuto 1)
   THEN (RWW "rabs-rmul<" 0 THENA Auto)
   THEN nRNorm 0
   THEN (RWO "rabs-difference-symmetry" (-1) THENA Auto)
   THEN nRNorm (-1)
   THEN (RWO "-1" 0 THENA 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))
⊢ (r1/r((k * k) * n)) ≤ (|v * v1|/r(n))

---

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/v)  -  (r1/v1)|  \mleq{}  (r1/r(n))


By

---

Latex:
((nRMul  \mkleeneopen{}|v|\mkleeneclose{}  0\mcdot{}  THENA  EAuto  1)
  THEN  (nRMul  \mkleeneopen{}|v1|\mkleeneclose{}  0\mcdot{}  THENA  EAuto  1)
  THEN  (RWW  "rabs-rmul<"  0  THENA  Auto)
  THEN  nRNorm  0
  THEN  (RWO  "rabs-difference-symmetry"  (-1)  THENA  Auto)
  THEN  nRNorm  (-1)
  THEN  (RWO  "-1"  0  THENA  Auto))\mcdot{}

---

Home Index