Step
*
2
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)) ∧ iproper(i-approx(I;n))
14. M : ℕ+
15. ∀x:{x:ℝ| x ∈ i-approx(I;n)} . ((|f1(x)| ≤ r(M)) ∧ (|f2(x)| ≤ r(M)) ∧ (|g2(x)| ≤ r(M)))
16. del : ℝ
17. [%14] : (r0 < del)
∧ (∀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|))))
18. d1 : ℝ
19. [%19] : (r0 < d1)
∧ (∀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|))))
20. d : ℝ
21. [%24] : (r0 < d)
∧ (∀x,y:ℝ. ((x ∈ i-approx(I;n)) ⇒ (y ∈ i-approx(I;n)) ⇒ (|x - y| ≤ d) ⇒ (|f1(x) - f1(y)| ≤ (r1/r((3 * M) * k)))))
⊢ ∃del:{ℝ| ((r0 < del)
∧ (∀x,y:ℝ.
((x ∈ i-approx(I;n))
⇒ (y ∈ i-approx(I;n))
⇒ (|y - x| ≤ del)
⇒ (|(f1[y] * f2[y]) - f1[x] * f2[x] - ((f1[x] * g2[x]) + (f2[x] * g1[x])) * (y - x)| ≤ ((r1/r(k))
* |y - x|)))))}
BY
{ (With ⌜rmin(del;rmin(d1;d))⌝ (D 0)⋅ THEN Auto) }
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))))
⊢ r0 < rmin(del;rmin(d1;d))
2
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))
⊢ |(f1[y] * f2[y]) - f1[x] * f2[x] - ((f1[x] * g2[x]) + (f2[x] * 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)) \mwedge{} iproper(i-approx(I;n))
14. M : \mBbbN{}\msupplus{}
15. \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)))
16. del : \mBbbR{}
17. [\%14] : (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{} (|f2[y] - f2[x] - g2[x] * (y - x)| \mleq{} ((r1/r((3 * M) * k)) * |y - x|))))
18. d1 : \mBbbR{}
19. [\%19] : (r0 < d1)
\mwedge{} (\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|))))
20. d : \mBbbR{}
21. [\%24] : (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{} (|f1(x) - f1(y)| \mleq{} (r1/r((3 * 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{} (|(f1[y] * f2[y]) - f1[x] * f2[x] - ((f1[x] * g2[x]) + (f2[x] * g1[x]))
* (y - x)| \mleq{} ((r1/r(k)) * |y - x|)))))\}
By
Latex:
(With \mkleeneopen{}rmin(del;rmin(d1;d))\mkleeneclose{} (D 0)\mcdot{} THEN Auto)
Home
Index