Step
*
1
2
1
of Lemma
derivative-rinv
1. I : Interval
2. f : I ⟶ℝ
3. g : I ⟶ℝ
4. ∀x,y:{t:ℝ| t ∈ I} . ((x = y) ⇒ (g[x] = g[y]))
5. k : ℕ+
6. n : {n:ℕ+| icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))}
7. ∀a,b:{x:ℝ| x ∈ i-approx(I;n)} . ((a = b) ⇒ (f[a] = f[b]))
8. i-approx(I;n) ⊆ I
9. ∀x:ℝ. ((x ∈ I) ⇒ f[x] ≠ r0)
10. ∃c:ℝ [((r0 < c) ∧ (∀x:ℝ. ((x ∈ i-approx(I;n)) ⇒ (c ≤ |f[x]|))))]
11. (r1/f[x]) continuous for x ∈ i-approx(I;n)
12. g[x] continuous for x ∈ i-approx(I;n)
13. ∀x:ℝ. ((x ∈ i-approx(I;n)) ⇒ f[x] ≠ r0)
14. M : ℕ+
15. ∀x:ℝ. ((x ∈ i-approx(I;n)) ⇒ ((|g[x]| ≤ r(M)) ∧ (|(r1/f[x])| ≤ r(M))))
16. del : ℝ
17. [%24] : (r0 < del)
∧ (∀x,y:ℝ.
((x ∈ i-approx(I;n))
⇒ (y ∈ i-approx(I;n))
⇒ (|y - x| ≤ del)
⇒ (|f[y] - f[x] - g[x] * (y - x)| ≤ ((r1/r((2 * M * M) * k)) * |y - x|))))
18. (2 * (M * M) * M * M) * k ∈ ℕ+
19. d : ℝ
20. [%33] : (r0 < d)
∧ (∀x,y:ℝ.
((x ∈ i-approx(I;n))
⇒ (y ∈ i-approx(I;n))
⇒ (|x - y| ≤ d)
⇒ (|f[x] - f[y]| ≤ (r1/r((2 * (M * M) * M * M) * k)))))
⊢ ∃del:ℝ [((r0 < del)
∧ (∀x,y:ℝ.
((x ∈ i-approx(I;n))
⇒ (y ∈ i-approx(I;n))
⇒ (|y - x| ≤ del)
⇒ (|(r1/f[y]) - (r1/f[x]) - (-(g[x])/f[x] * f[x]) * (y - x)| ≤ ((r1/r(k)) * |y - x|)))))]
BY
{ (With ⌜rmin(del;d)⌝ (D 0)⋅ THEN Auto) }
1
1. I : Interval
2. f : I ⟶ℝ
3. g : I ⟶ℝ
4. ∀x,y:{t:ℝ| t ∈ I} . ((x = y) ⇒ (g[x] = g[y]))
5. k : ℕ+
6. n : {n:ℕ+| icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))}
7. ∀a,b:{x:ℝ| x ∈ i-approx(I;n)} . ((a = b) ⇒ (f[a] = f[b]))
8. i-approx(I;n) ⊆ I
9. ∀x:ℝ. ((x ∈ I) ⇒ f[x] ≠ r0)
10. ∃c:ℝ [((r0 < c) ∧ (∀x:ℝ. ((x ∈ i-approx(I;n)) ⇒ (c ≤ |f[x]|))))]
11. (r1/f[x]) continuous for x ∈ i-approx(I;n)
12. g[x] continuous for x ∈ i-approx(I;n)
13. ∀x:ℝ. ((x ∈ i-approx(I;n)) ⇒ f[x] ≠ r0)
14. M : ℕ+
15. ∀x:ℝ. ((x ∈ i-approx(I;n)) ⇒ ((|g[x]| ≤ r(M)) ∧ (|(r1/f[x])| ≤ r(M))))
16. del : ℝ
17. r0 < del
18. ∀x,y:ℝ.
((x ∈ i-approx(I;n))
⇒ (y ∈ i-approx(I;n))
⇒ (|y - x| ≤ del)
⇒ (|f[y] - f[x] - g[x] * (y - x)| ≤ ((r1/r((2 * M * M) * k)) * |y - x|)))
19. (2 * (M * M) * M * M) * k ∈ ℕ+
20. d : ℝ
21. r0 < d
22. ∀x,y:ℝ.
((x ∈ i-approx(I;n))
⇒ (y ∈ i-approx(I;n))
⇒ (|x - y| ≤ d)
⇒ (|f[x] - f[y]| ≤ (r1/r((2 * (M * M) * M * M) * k))))
⊢ r0 < rmin(del;d)
2
1. I : Interval
2. f : I ⟶ℝ
3. g : I ⟶ℝ
4. ∀x,y:{t:ℝ| t ∈ I} . ((x = y) ⇒ (g[x] = g[y]))
5. k : ℕ+
6. n : {n:ℕ+| icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))}
7. ∀a,b:{x:ℝ| x ∈ i-approx(I;n)} . ((a = b) ⇒ (f[a] = f[b]))
8. i-approx(I;n) ⊆ I
9. ∀x:ℝ. ((x ∈ I) ⇒ f[x] ≠ r0)
10. ∃c:ℝ [((r0 < c) ∧ (∀x:ℝ. ((x ∈ i-approx(I;n)) ⇒ (c ≤ |f[x]|))))]
11. (r1/f[x]) continuous for x ∈ i-approx(I;n)
12. g[x] continuous for x ∈ i-approx(I;n)
13. ∀x:ℝ. ((x ∈ i-approx(I;n)) ⇒ f[x] ≠ r0)
14. M : ℕ+
15. ∀x:ℝ. ((x ∈ i-approx(I;n)) ⇒ ((|g[x]| ≤ r(M)) ∧ (|(r1/f[x])| ≤ r(M))))
16. del : ℝ
17. r0 < del
18. ∀x,y:ℝ.
((x ∈ i-approx(I;n))
⇒ (y ∈ i-approx(I;n))
⇒ (|y - x| ≤ del)
⇒ (|f[y] - f[x] - g[x] * (y - x)| ≤ ((r1/r((2 * M * M) * k)) * |y - x|)))
19. (2 * (M * M) * M * M) * k ∈ ℕ+
20. d : ℝ
21. r0 < d
22. ∀x,y:ℝ.
((x ∈ i-approx(I;n))
⇒ (y ∈ i-approx(I;n))
⇒ (|x - y| ≤ d)
⇒ (|f[x] - f[y]| ≤ (r1/r((2 * (M * M) * M * M) * k))))
23. r0 < rmin(del;d)
24. x : ℝ
25. y : ℝ
26. x ∈ i-approx(I;n)
27. y ∈ i-approx(I;n)
28. |y - x| ≤ rmin(del;d)
⊢ |(r1/f[y]) - (r1/f[x]) - (-(g[x])/f[x] * f[x]) * (y - x)| ≤ ((r1/r(k)) * |y - x|)
3
1. I : Interval
2. f : I ⟶ℝ
3. g : I ⟶ℝ
4. ∀x,y:{t:ℝ| t ∈ I} . ((x = y) ⇒ (g[x] = g[y]))
5. k : ℕ+
6. n : {n:ℕ+| icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))}
7. ∀a,b:{x:ℝ| x ∈ i-approx(I;n)} . ((a = b) ⇒ (f[a] = f[b]))
8. i-approx(I;n) ⊆ I
9. ∀x:ℝ. ((x ∈ I) ⇒ f[x] ≠ r0)
10. ∃c:ℝ [((r0 < c) ∧ (∀x:ℝ. ((x ∈ i-approx(I;n)) ⇒ (c ≤ |f[x]|))))]
11. (r1/f[x]) continuous for x ∈ i-approx(I;n)
12. g[x] continuous for x ∈ i-approx(I;n)
13. ∀x:ℝ. ((x ∈ i-approx(I;n)) ⇒ f[x] ≠ r0)
14. M : ℕ+
15. ∀x:ℝ. ((x ∈ i-approx(I;n)) ⇒ ((|g[x]| ≤ r(M)) ∧ (|(r1/f[x])| ≤ r(M))))
16. del : ℝ
17. r0 < del
18. ∀x,y:ℝ.
((x ∈ i-approx(I;n))
⇒ (y ∈ i-approx(I;n))
⇒ (|y - x| ≤ del)
⇒ (|f[y] - f[x] - g[x] * (y - x)| ≤ ((r1/r((2 * M * M) * k)) * |y - x|)))
19. (2 * (M * M) * M * M) * k ∈ ℕ+
20. d : ℝ
21. r0 < d
22. ∀x,y:ℝ.
((x ∈ i-approx(I;n))
⇒ (y ∈ i-approx(I;n))
⇒ (|x - y| ≤ d)
⇒ (|f[x] - f[y]| ≤ (r1/r((2 * (M * M) * M * M) * k))))
23. d1 : ℝ
24. x : r0 < d1
25. x1 : ℝ
26. y : ℝ
27. x2 : x1 ∈ i-approx(I;n)
28. x3 : y ∈ i-approx(I;n)
29. x4 : |y - x1| ≤ d1
⊢ f[x1] * f[x1] ≠ r0
Latex:
Latex:
1. I : Interval
2. f : I {}\mrightarrow{}\mBbbR{}
3. g : I {}\mrightarrow{}\mBbbR{}
4. \mforall{}x,y:\{t:\mBbbR{}| t \mmember{} I\} . ((x = y) {}\mRightarrow{} (g[x] = g[y]))
5. k : \mBbbN{}\msupplus{}
6. n : \{n:\mBbbN{}\msupplus{}| icompact(i-approx(I;n)) \mwedge{} iproper(i-approx(I;n))\}
7. \mforall{}a,b:\{x:\mBbbR{}| x \mmember{} i-approx(I;n)\} . ((a = b) {}\mRightarrow{} (f[a] = f[b]))
8. i-approx(I;n) \msubseteq{} I
9. \mforall{}x:\mBbbR{}. ((x \mmember{} I) {}\mRightarrow{} f[x] \mneq{} r0)
10. \mexists{}c:\mBbbR{} [((r0 < c) \mwedge{} (\mforall{}x:\mBbbR{}. ((x \mmember{} i-approx(I;n)) {}\mRightarrow{} (c \mleq{} |f[x]|))))]
11. (r1/f[x]) continuous for x \mmember{} i-approx(I;n)
12. g[x] continuous for x \mmember{} i-approx(I;n)
13. \mforall{}x:\mBbbR{}. ((x \mmember{} i-approx(I;n)) {}\mRightarrow{} f[x] \mneq{} r0)
14. M : \mBbbN{}\msupplus{}
15. \mforall{}x:\mBbbR{}. ((x \mmember{} i-approx(I;n)) {}\mRightarrow{} ((|g[x]| \mleq{} r(M)) \mwedge{} (|(r1/f[x])| \mleq{} r(M))))
16. del : \mBbbR{}
17. [\%24] : (r0 < del)
\mwedge{} (\mforall{}x,y:\mBbbR{}.
((x \mmember{} i-approx(I;n))
{}\mRightarrow{} (y \mmember{} i-approx(I;n))
{}\mRightarrow{} (|y - x| \mleq{} del)
{}\mRightarrow{} (|f[y] - f[x] - g[x] * (y - x)| \mleq{} ((r1/r((2 * M * M) * k)) * |y - x|))))
18. (2 * (M * M) * M * M) * k \mmember{} \mBbbN{}\msupplus{}
19. d : \mBbbR{}
20. [\%33] : (r0 < d)
\mwedge{} (\mforall{}x,y:\mBbbR{}.
((x \mmember{} i-approx(I;n))
{}\mRightarrow{} (y \mmember{} i-approx(I;n))
{}\mRightarrow{} (|x - y| \mleq{} d)
{}\mRightarrow{} (|f[x] - f[y]| \mleq{} (r1/r((2 * (M * M) * M * M) * k)))))
\mvdash{} \mexists{}del:\mBbbR{} [((r0 < del)
\mwedge{} (\mforall{}x,y:\mBbbR{}.
((x \mmember{} i-approx(I;n))
{}\mRightarrow{} (y \mmember{} i-approx(I;n))
{}\mRightarrow{} (|y - x| \mleq{} del)
{}\mRightarrow{} (|(r1/f[y]) - (r1/f[x]) - (-(g[x])/f[x] * f[x]) * (y - x)| \mleq{} ((r1/r(k))
* |y - x|)))))]
By
Latex:
(With \mkleeneopen{}rmin(del;d)\mkleeneclose{} (D 0)\mcdot{} THEN Auto)
Home
Index