---

Step * 1 2 1 2 1 1 1 1 1 2 1 2 1 2 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|)
18. v : ℝ
19. (fy - fx - (fy * (r1/fx)) * gx * e) = v ∈ ℝ
20. v1 : ℝ
21. (|gx| * |(r1/fx)|) = v1 ∈ ℝ
22. v2 : ℝ
23. |fx - fy| = v2 ∈ ℝ
⊢ (|v| ≤ (((r1/r((2 * M * M) * k)) * |e|) + (v1 * v2 * |e|)))
⇒ ((v1 * v2) ≤ (r1/r((2 * M * M) * k)))
⇒ ((r(M * M) * |v|) ≤ ((r1/r(k)) * |e|))
BY
{ (All Thin THEN Auto) }

1
1. k : ℕ+
2. M : ℕ+
3. e : ℝ
4. v : ℝ
5. v1 : ℝ
6. v2 : ℝ
7. |v| ≤ (((r1/r((2 * M * M) * k)) * |e|) + (v1 * v2 * |e|))
8. (v1 * v2) ≤ (r1/r((2 * M * M) * k))
⊢ (r(M * M) * |v|) ≤ ((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|)
18.  v  :  \mBbbR{}
19.  (fy  -  fx  -  (fy  *  (r1/fx))  *  gx  *  e)  =  v
20.  v1  :  \mBbbR{}
21.  (|gx|  *  |(r1/fx)|)  =  v1
22.  v2  :  \mBbbR{}
23.  |fx  -  fy|  =  v2
\mvdash{}  (|v|  \mleq{}  (((r1/r((2  *  M  *  M)  *  k))  *  |e|)  +  (v1  *  v2  *  |e|)))
{}\mRightarrow{}  ((v1  *  v2)  \mleq{}  (r1/r((2  *  M  *  M)  *  k)))
{}\mRightarrow{}  ((r(M  *  M)  *  |v|)  \mleq{}  ((r1/r(k))  *  |e|))


By

---

Latex:
(All  Thin  THEN  Auto)

---

Home Index