---

Step * 1 2 1 2 1 1 1 of Lemma derivative-rinv


1. k : ℕ+
2. M : ℕ+
3. fx : ℝ
4. fy : ℝ
5. gx : ℝ
6. gy : ℝ
7. e : ℝ
8. fx ≠ r0
9. fy ≠ r0
10. |fy - fx - gx * e| ≤ ((r1/r((2 * M * M) * k)) * |e|)
11. |fy - fx| ≤ (r1/r((2 * (M * M) * M * M) * k))
12. |gx| ≤ r(M)
13. |(r1/fx)| ≤ r(M)
14. |gy| ≤ r(M)
15. |(r1/fy)| ≤ r(M)
16. fx * fx ≠ r0
17. |(r1/fy) - (r1/fx) - (-(gx)/fx * fx) * e| = ((|(r1/fx)| * |(r1/fy)|) * |fy - fx - (fy * (r1/fx)) * gx * e|)
⊢ |(r1/fy) - (r1/fx) - (-(gx)/fx * fx) * e| ≤ ((r1/r(k)) * |e|)
BY
{ (RWO "-1" 0 THENA Auto) }

1
1. k : ℕ+
2. M : ℕ+
3. fx : ℝ
4. fy : ℝ
5. gx : ℝ
6. gy : ℝ
7. e : ℝ
8. fx ≠ r0
9. fy ≠ r0
10. |fy - fx - gx * e| ≤ ((r1/r((2 * M * M) * k)) * |e|)
11. |fy - fx| ≤ (r1/r((2 * (M * M) * M * M) * k))
12. |gx| ≤ r(M)
13. |(r1/fx)| ≤ r(M)
14. |gy| ≤ r(M)
15. |(r1/fy)| ≤ r(M)
16. fx * fx ≠ r0
17. |(r1/fy) - (r1/fx) - (-(gx)/fx * fx) * e| = ((|(r1/fx)| * |(r1/fy)|) * |fy - fx - (fy * (r1/fx)) * gx * e|)
⊢ ((|(r1/fx)| * |(r1/fy)|) * |fy - fx - (fy * (r1/fx)) * gx * e|) ≤ ((r1/r(k)) * |e|)

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
2.  M  :  \mBbbN{}\msupplus{}
3.  fx  :  \mBbbR{}
4.  fy  :  \mBbbR{}
5.  gx  :  \mBbbR{}
6.  gy  :  \mBbbR{}
7.  e  :  \mBbbR{}
8.  fx  \mneq{}  r0
9.  fy  \mneq{}  r0
10.  |fy  -  fx  -  gx  *  e|  \mleq{}  ((r1/r((2  *  M  *  M)  *  k))  *  |e|)
11.  |fy  -  fx|  \mleq{}  (r1/r((2  *  (M  *  M)  *  M  *  M)  *  k))
12.  |gx|  \mleq{}  r(M)
13.  |(r1/fx)|  \mleq{}  r(M)
14.  |gy|  \mleq{}  r(M)
15.  |(r1/fy)|  \mleq{}  r(M)
16.  fx  *  fx  \mneq{}  r0
17.  |(r1/fy)  -  (r1/fx)  -  (-(gx)/fx  *  fx)  *  e|
=  ((|(r1/fx)|  *  |(r1/fy)|)  *  |fy  -  fx  -  (fy  *  (r1/fx))  *  gx  *  e|)
\mvdash{}  |(r1/fy)  -  (r1/fx)  -  (-(gx)/fx  *  fx)  *  e|  \mleq{}  ((r1/r(k))  *  |e|)


By

---

Latex:
(RWO  "-1"  0  THENA  Auto)

---

Home Index