Step
*
2
1
2
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))
⊢ |(f1[y] * f2[y]) - f1[x] * f2[x] - ((f1[x] * g2[x]) + (f2[x] * g1[x])) * (y - x)| ≤ ((r1/r(k)) * |y - x|)
BY
{ ((Assert |(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)|)) BY
(((GenConclTerm ⌜f1[y]⌝⋅ THENA Auto) THEN (GenConclTerm ⌜f1[x]⌝⋅ THENA Auto))
THEN ((GenConclTerm ⌜f2[y]⌝⋅ THENA Auto) THEN (GenConclTerm ⌜f2[x]⌝⋅ THENA Auto))
THEN (GenConclTerm ⌜g2[x]⌝⋅ THENA Auto)
THEN ((GenConclTerm ⌜g1[x]⌝⋅ THENA Auto) THEN (GenConclTerm ⌜y - x⌝⋅ THENA Auto))
THEN All Thin
THEN (RWW "rabs-rmul< r-triangle-inequality<" 0⋅ THENA Auto)⋅
THEN nRNorm 0
THEN Auto))
THEN (RWO "-1" 0 THENA 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))))
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]| * |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|)
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))
\mvdash{} |(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:
((Assert |(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)|)) BY
(((GenConclTerm \mkleeneopen{}f1[y]\mkleeneclose{}\mcdot{} THENA Auto) THEN (GenConclTerm \mkleeneopen{}f1[x]\mkleeneclose{}\mcdot{} THENA Auto))
THEN ((GenConclTerm \mkleeneopen{}f2[y]\mkleeneclose{}\mcdot{} THENA Auto) THEN (GenConclTerm \mkleeneopen{}f2[x]\mkleeneclose{}\mcdot{} THENA Auto))
THEN (GenConclTerm \mkleeneopen{}g2[x]\mkleeneclose{}\mcdot{} THENA Auto)
THEN ((GenConclTerm \mkleeneopen{}g1[x]\mkleeneclose{}\mcdot{} THENA Auto) THEN (GenConclTerm \mkleeneopen{}y - x\mkleeneclose{}\mcdot{} THENA Auto))
THEN All Thin
THEN (RWW "rabs-rmul< r-triangle-inequality<" 0\mcdot{} THENA Auto)\mcdot{}
THEN nRNorm 0
THEN Auto))
THEN (RWO "-1" 0 THENA Auto)
)
Home
Index