Step
*
2
1
2
1
1
1
1
of Lemma
derivative-mul-part1
1. I : Interval
2. True
3. f1 : I ⟶ℝ
4. f2 : I ⟶ℝ
5. g1 : I ⟶ℝ
6. g2 : I ⟶ℝ
7. ∀m:{m:ℕ+| icompact(i-approx(I;m)) ∧ iproper(i-approx(I;m))} . ∀n:ℕ+.
(∃d:{ℝ| ((r0 < d)
∧ (∀x,y:ℝ.
((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d) ⇒ (|f1(x) - f1(y)| ≤ (r1/r(n))))))})
8. f2(x) (proper)continuous for x ∈ I
9. g2(x) (proper)continuous for x ∈ I
10. k : ℕ+
11. n : {n:ℕ+| icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))}
12. i-approx(I;n) ⊆ I
13. icompact(i-approx(I;n))
14. iproper(i-approx(I;n))
15. M : ℕ+
16. ∀x:{x:ℝ| x ∈ i-approx(I;n)} . ((|f1(x)| ≤ r(M)) ∧ (|f2(x)| ≤ r(M)) ∧ (|g2(x)| ≤ r(M)))
17. del : ℝ
18. r0 < del
19. ∀x,y:ℝ.
((x ∈ i-approx(I;n))
⇒ (y ∈ i-approx(I;n))
⇒ (|y - x| ≤ del)
⇒ (|f2[y] - f2[x] - g2[x] * (y - x)| ≤ ((r1/r((3 * M) * k)) * |y - x|)))
20. d1 : ℝ
21. r0 < d1
22. ∀x,y:ℝ.
((x ∈ i-approx(I;n))
⇒ (y ∈ i-approx(I;n))
⇒ (|y - x| ≤ d1)
⇒ (|f1[y] - f1[x] - g1[x] * (y - x)| ≤ ((r1/r((3 * M) * k)) * |y - x|)))
23. d : ℝ
24. r0 < d
25. ∀x,y:ℝ. ((x ∈ i-approx(I;n)) ⇒ (y ∈ i-approx(I;n)) ⇒ (|x - y| ≤ d) ⇒ (|f1(x) - f1(y)| ≤ (r1/r((3 * M) * k))))
26. r0 < rmin(del;rmin(d1;d))
27. x : ℝ
28. y : ℝ
29. x ∈ i-approx(I;n)
30. y ∈ i-approx(I;n)
31. |y - x| ≤ rmin(del;rmin(d1;d))
32. |(f1[y] * f2[y]) - f1[x] * f2[x] - ((f1[x] * g2[x]) + (f2[x] * g1[x])) * (y - x)| ≤ ((|f1[y]|
* |f2[y] - f2[x] - g2[x]
* (y - x)|)
+ (|f1[y] - f1[x]| * |g2[x]| * |y - x|)
+ (|f2[x]| * |f1[y] - f1[x] - g1[x] * (y - x)|))
⊢ ((|f1(y)| ≤ r(M)) ∧ (|f2(y)| ≤ r(M)) ∧ (|g2(y)| ≤ r(M)))
⇒ ((|f1(x)| ≤ r(M)) ∧ (|f2(x)| ≤ r(M)) ∧ (|g2(x)| ≤ r(M)))
⇒ (|f1(y) - f1(x)| ≤ (r1/r((3 * M) * k)))
⇒ (|f1[y] - f1[x] - g1[x] * (y - x)| ≤ ((r1/r((3 * M) * k)) * |y - x|))
⇒ (|f2[y] - f2[x] - g2[x] * (y - x)| ≤ ((r1/r((3 * M) * k)) * |y - x|))
⇒ (((|f1[y]| * |f2[y] - f2[x] - g2[x] * (y - x)|)
+ (|f1[y] - f1[x]| * |g2[x]| * |y - x|)
+ (|f2[x]| * |f1[y] - f1[x] - g1[x] * (y - x)|)) ≤ ((r1/r(k)) * |y - x|))
BY
{ ((Unfold `so_apply` 0 THEN Fold `r-ap` 0)
THEN GenConclAtAddr [1;1;1;1]⋅
THEN GenConclAtAddr [1;2;1;1;1]⋅
THEN GenConclAtAddr [1;2;2;1;1]⋅
THEN (D 0 THENA Auto)
THEN GenConclAtAddr [1;1;1;1]⋅
THEN GenConclAtAddr [1;2;1;1;1]⋅
THEN GenConclAtAddr [1;2;2;1;1]⋅) }
1
1. I : Interval
2. True
3. f1 : I ⟶ℝ
4. f2 : I ⟶ℝ
5. g1 : I ⟶ℝ
6. g2 : I ⟶ℝ
7. ∀m:{m:ℕ+| icompact(i-approx(I;m)) ∧ iproper(i-approx(I;m))} . ∀n:ℕ+.
(∃d:{ℝ| ((r0 < d)
∧ (∀x,y:ℝ.
((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d) ⇒ (|f1(x) - f1(y)| ≤ (r1/r(n))))))})
8. f2(x) (proper)continuous for x ∈ I
9. g2(x) (proper)continuous for x ∈ I
10. k : ℕ+
11. n : {n:ℕ+| icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))}
12. i-approx(I;n) ⊆ I
13. icompact(i-approx(I;n))
14. iproper(i-approx(I;n))
15. M : ℕ+
16. ∀x:{x:ℝ| x ∈ i-approx(I;n)} . ((|f1(x)| ≤ r(M)) ∧ (|f2(x)| ≤ r(M)) ∧ (|g2(x)| ≤ r(M)))
17. del : ℝ
18. r0 < del
19. ∀x,y:ℝ.
((x ∈ i-approx(I;n))
⇒ (y ∈ i-approx(I;n))
⇒ (|y - x| ≤ del)
⇒ (|f2[y] - f2[x] - g2[x] * (y - x)| ≤ ((r1/r((3 * M) * k)) * |y - x|)))
20. d1 : ℝ
21. r0 < d1
22. ∀x,y:ℝ.
((x ∈ i-approx(I;n))
⇒ (y ∈ i-approx(I;n))
⇒ (|y - x| ≤ d1)
⇒ (|f1[y] - f1[x] - g1[x] * (y - x)| ≤ ((r1/r((3 * M) * k)) * |y - x|)))
23. d : ℝ
24. r0 < d
25. ∀x,y:ℝ. ((x ∈ i-approx(I;n)) ⇒ (y ∈ i-approx(I;n)) ⇒ (|x - y| ≤ d) ⇒ (|f1(x) - f1(y)| ≤ (r1/r((3 * M) * k))))
26. r0 < rmin(del;rmin(d1;d))
27. x : ℝ
28. y : ℝ
29. x ∈ i-approx(I;n)
30. y ∈ i-approx(I;n)
31. |y - x| ≤ rmin(del;rmin(d1;d))
32. |(f1[y] * f2[y]) - f1[x] * f2[x] - ((f1[x] * g2[x]) + (f2[x] * g1[x])) * (y - x)| ≤ ((|f1[y]|
* |f2[y] - f2[x] - g2[x]
* (y - x)|)
+ (|f1[y] - f1[x]| * |g2[x]| * |y - x|)
+ (|f2[x]| * |f1[y] - f1[x] - g1[x] * (y - x)|))
33. v : ℝ
34. f1(y) = v ∈ ℝ
35. v1 : ℝ
36. f2(y) = v1 ∈ ℝ
37. v2 : ℝ
38. g2(y) = v2 ∈ ℝ
39. (|v| ≤ r(M)) ∧ (|v1| ≤ r(M)) ∧ (|v2| ≤ r(M))
40. v3 : ℝ
41. f1(x) = v3 ∈ ℝ
42. v4 : ℝ
43. f2(x) = v4 ∈ ℝ
44. v5 : ℝ
45. g2(x) = v5 ∈ ℝ
⊢ ((|v3| ≤ r(M)) ∧ (|v4| ≤ r(M)) ∧ (|v5| ≤ r(M)))
⇒ (|v - v3| ≤ (r1/r((3 * M) * k)))
⇒ (|v - v3 - g1(x) * (y - x)| ≤ ((r1/r((3 * M) * k)) * |y - x|))
⇒ (|v1 - v4 - v5 * (y - x)| ≤ ((r1/r((3 * M) * k)) * |y - x|))
⇒ (((|v| * |v1 - v4 - v5 * (y - x)|) + (|v - v3| * |v5| * |y - x|) + (|v4| * |v - v3 - g1(x) * (y - x)|)) ≤ ((r1/r(k))
* |y - x|))
Latex:
Latex:
1. I : Interval
2. True
3. f1 : I {}\mrightarrow{}\mBbbR{}
4. f2 : I {}\mrightarrow{}\mBbbR{}
5. g1 : I {}\mrightarrow{}\mBbbR{}
6. g2 : I {}\mrightarrow{}\mBbbR{}
7. \mforall{}m:\{m:\mBbbN{}\msupplus{}| icompact(i-approx(I;m)) \mwedge{} iproper(i-approx(I;m))\} . \mforall{}n:\mBbbN{}\msupplus{}.
(\mexists{}d:\{\mBbbR{}| ((r0 < d)
\mwedge{} (\mforall{}x,y:\mBbbR{}.
((x \mmember{} i-approx(I;m))
{}\mRightarrow{} (y \mmember{} i-approx(I;m))
{}\mRightarrow{} (|x - y| \mleq{} d)
{}\mRightarrow{} (|f1(x) - f1(y)| \mleq{} (r1/r(n))))))\})
8. f2(x) (proper)continuous for x \mmember{} I
9. g2(x) (proper)continuous for x \mmember{} I
10. k : \mBbbN{}\msupplus{}
11. n : \{n:\mBbbN{}\msupplus{}| icompact(i-approx(I;n)) \mwedge{} iproper(i-approx(I;n))\}
12. i-approx(I;n) \msubseteq{} I
13. icompact(i-approx(I;n))
14. iproper(i-approx(I;n))
15. M : \mBbbN{}\msupplus{}
16. \mforall{}x:\{x:\mBbbR{}| x \mmember{} i-approx(I;n)\} . ((|f1(x)| \mleq{} r(M)) \mwedge{} (|f2(x)| \mleq{} r(M)) \mwedge{} (|g2(x)| \mleq{} r(M)))
17. del : \mBbbR{}
18. r0 < del
19. \mforall{}x,y:\mBbbR{}.
((x \mmember{} i-approx(I;n))
{}\mRightarrow{} (y \mmember{} i-approx(I;n))
{}\mRightarrow{} (|y - x| \mleq{} del)
{}\mRightarrow{} (|f2[y] - f2[x] - g2[x] * (y - x)| \mleq{} ((r1/r((3 * M) * k)) * |y - x|)))
20. d1 : \mBbbR{}
21. r0 < d1
22. \mforall{}x,y:\mBbbR{}.
((x \mmember{} i-approx(I;n))
{}\mRightarrow{} (y \mmember{} i-approx(I;n))
{}\mRightarrow{} (|y - x| \mleq{} d1)
{}\mRightarrow{} (|f1[y] - f1[x] - g1[x] * (y - x)| \mleq{} ((r1/r((3 * M) * k)) * |y - x|)))
23. d : \mBbbR{}
24. r0 < d
25. \mforall{}x,y:\mBbbR{}.
((x \mmember{} i-approx(I;n))
{}\mRightarrow{} (y \mmember{} i-approx(I;n))
{}\mRightarrow{} (|x - y| \mleq{} d)
{}\mRightarrow{} (|f1(x) - f1(y)| \mleq{} (r1/r((3 * M) * k))))
26. r0 < rmin(del;rmin(d1;d))
27. x : \mBbbR{}
28. y : \mBbbR{}
29. x \mmember{} i-approx(I;n)
30. y \mmember{} i-approx(I;n)
31. |y - x| \mleq{} rmin(del;rmin(d1;d))
32. |(f1[y] * f2[y]) - f1[x] * f2[x] - ((f1[x] * g2[x]) + (f2[x] * g1[x])) * (y - x)| \mleq{} ((|f1[y]|
* |f2[y]
- f2[x]
- g2[x]
* (y
- x)|)
+ (|f1[y] - f1[x]| * |g2[x]| * |y - x|)
+ (|f2[x]| * |f1[y] - f1[x] - g1[x] * (y - x)|))
\mvdash{} ((|f1(y)| \mleq{} r(M)) \mwedge{} (|f2(y)| \mleq{} r(M)) \mwedge{} (|g2(y)| \mleq{} r(M)))
{}\mRightarrow{} ((|f1(x)| \mleq{} r(M)) \mwedge{} (|f2(x)| \mleq{} r(M)) \mwedge{} (|g2(x)| \mleq{} r(M)))
{}\mRightarrow{} (|f1(y) - f1(x)| \mleq{} (r1/r((3 * M) * k)))
{}\mRightarrow{} (|f1[y] - f1[x] - g1[x] * (y - x)| \mleq{} ((r1/r((3 * M) * k)) * |y - x|))
{}\mRightarrow{} (|f2[y] - f2[x] - g2[x] * (y - x)| \mleq{} ((r1/r((3 * M) * k)) * |y - x|))
{}\mRightarrow{} (((|f1[y]| * |f2[y] - f2[x] - g2[x] * (y - x)|)
+ (|f1[y] - f1[x]| * |g2[x]| * |y - x|)
+ (|f2[x]| * |f1[y] - f1[x] - g1[x] * (y - x)|)) \mleq{} ((r1/r(k)) * |y - x|))
By
Latex:
((Unfold `so\_apply` 0 THEN Fold `r-ap` 0)
THEN GenConclAtAddr [1;1;1;1]\mcdot{}
THEN GenConclAtAddr [1;2;1;1;1]\mcdot{}
THEN GenConclAtAddr [1;2;2;1;1]\mcdot{}
THEN (D 0 THENA Auto)
THEN GenConclAtAddr [1;1;1;1]\mcdot{}
THEN GenConclAtAddr [1;2;1;1;1]\mcdot{}
THEN GenConclAtAddr [1;2;2;1;1]\mcdot{})
Home
Index