Step
*
1
1
2
1
1
2
of Lemma
chain-rule_1
1. I : Interval@i
2. J : Interval@i
3. f : I ⟶ℝ@i
4. f' : I ⟶ℝ@i
5. g : J ⟶ℝ@i
6. g' : J ⟶ℝ@i
7. f[x] continuous for x ∈ I@i
8. f'[x] continuous for x ∈ I@i
9. g'[x] continuous for x ∈ J@i
10. λx.g'[x] = d(g[x])/dx on J@i
11. k : ℕ+@i
12. n : {n:ℕ+| icompact(i-approx(I;n))} @i
13. m : {m:ℕ+| icompact(i-approx(J;m))} @i
14. ∀x:{x:ℝ| x ∈ i-approx(I;n)} . (f[x] ∈ i-approx(J;m))@i
15. mc1 : f'[x] continuous for x ∈ i-approx(I;n)
16. ∃a:ℝ. ∀[x:{r:ℝ| r ∈ i-approx(I;n)} ]. (|f'[x]| ≤ a)
17. mc2 : g'[x] continuous for x ∈ i-approx(J;m)
18. ∃b:ℝ. ∀[x:{r:ℝ| r ∈ i-approx(J;m)} ]. (|g'[x]| ≤ b)
19. f' ∈ i-approx(I;n) ⟶ℝ
20. A : ℕ+
21. ∀r:ℝ. ((r ∈ i-approx(I;n)) ⇒ (|f'[r]| ≤ (r(A)/r(2 * k))))
22. g ∈ i-approx(J;m) ⟶ℝ
23. g' ∈ i-approx(J;m) ⟶ℝ
24. f ∈ i-approx(I;n) ⟶ℝ
25. d : ℝ
26. r0 < d
27. ∀x,y:ℝ.
((x ∈ i-approx(I;n))
⇒ (y ∈ i-approx(I;n))
⇒ (|y - x| ≤ d)
⇒ (|g[f[y]] - g[f[x]] - g'[f[x]] * (f[y] - f[x])| ≤ ((r1/r(A)) * |f[y] - f[x]|)))
28. B : ℕ+
29. ∀r:ℝ. ((r ∈ i-approx(J;m)) ⇒ (((r1/r(A)) + |g'[r]|) ≤ (r(B)/r(2 * k))))
30. del : ℝ@i
31. r0 < del@i
32. ∀x,y:ℝ.
((x ∈ i-approx(I;n))
⇒ (y ∈ i-approx(I;n))
⇒ (|y - x| ≤ del)
⇒ (|f[y] - f[x] - f'[x] * (y - x)| ≤ ((r1/r(B)) * |y - x|)))@i
33. r0 < rmin(d;del)
34. x : ℝ@i
35. y : ℝ@i
36. x ∈ i-approx(I;n)@i
37. y ∈ i-approx(I;n)@i
38. |y - x| ≤ rmin(d;del)@i
⊢ |g[f[y]] - g[f[x]] - (g'[f[x]] * f'[x]) * (y - x)| ≤ ((r1/r(k)) * |y - x|)
BY
{ ((Assert (|y - x| ≤ d) ∧ (|y - x| ≤ del) BY
(RWO "-1" 0 THEN Auto))
THEN D -1
THEN RepeatFor 2 (∀h:hyp. (FHyp h [-2] THENA Auto) )) }
1
1. I : Interval@i
2. J : Interval@i
3. f : I ⟶ℝ@i
4. f' : I ⟶ℝ@i
5. g : J ⟶ℝ@i
6. g' : J ⟶ℝ@i
7. f[x] continuous for x ∈ I@i
8. f'[x] continuous for x ∈ I@i
9. g'[x] continuous for x ∈ J@i
10. λx.g'[x] = d(g[x])/dx on J@i
11. k : ℕ+@i
12. n : {n:ℕ+| icompact(i-approx(I;n))} @i
13. m : {m:ℕ+| icompact(i-approx(J;m))} @i
14. ∀x:{x:ℝ| x ∈ i-approx(I;n)} . (f[x] ∈ i-approx(J;m))@i
15. mc1 : f'[x] continuous for x ∈ i-approx(I;n)
16. ∃a:ℝ. ∀[x:{r:ℝ| r ∈ i-approx(I;n)} ]. (|f'[x]| ≤ a)
17. mc2 : g'[x] continuous for x ∈ i-approx(J;m)
18. ∃b:ℝ. ∀[x:{r:ℝ| r ∈ i-approx(J;m)} ]. (|g'[x]| ≤ b)
19. f' ∈ i-approx(I;n) ⟶ℝ
20. A : ℕ+
21. ∀r:ℝ. ((r ∈ i-approx(I;n)) ⇒ (|f'[r]| ≤ (r(A)/r(2 * k))))
22. g ∈ i-approx(J;m) ⟶ℝ
23. g' ∈ i-approx(J;m) ⟶ℝ
24. f ∈ i-approx(I;n) ⟶ℝ
25. d : ℝ
26. r0 < d
27. ∀x,y:ℝ.
((x ∈ i-approx(I;n))
⇒ (y ∈ i-approx(I;n))
⇒ (|y - x| ≤ d)
⇒ (|g[f[y]] - g[f[x]] - g'[f[x]] * (f[y] - f[x])| ≤ ((r1/r(A)) * |f[y] - f[x]|)))
28. B : ℕ+
29. ∀r:ℝ. ((r ∈ i-approx(J;m)) ⇒ (((r1/r(A)) + |g'[r]|) ≤ (r(B)/r(2 * k))))
30. del : ℝ@i
31. r0 < del@i
32. ∀x,y:ℝ.
((x ∈ i-approx(I;n))
⇒ (y ∈ i-approx(I;n))
⇒ (|y - x| ≤ del)
⇒ (|f[y] - f[x] - f'[x] * (y - x)| ≤ ((r1/r(B)) * |y - x|)))@i
33. r0 < rmin(d;del)
34. x : ℝ@i
35. y : ℝ@i
36. x ∈ i-approx(I;n)@i
37. y ∈ i-approx(I;n)@i
38. |y - x| ≤ rmin(d;del)@i
39. |y - x| ≤ d
40. |y - x| ≤ del
41. |g[f[y]] - g[f[x]] - g'[f[x]] * (f[y] - f[x])| ≤ ((r1/r(A)) * |f[y] - f[x]|)
42. |f[y] - f[x] - f'[x] * (y - x)| ≤ ((r1/r(B)) * |y - x|)
⊢ |g[f[y]] - g[f[x]] - (g'[f[x]] * f'[x]) * (y - x)| ≤ ((r1/r(k)) * |y - x|)
Latex:
Latex:
1. I : Interval@i
2. J : Interval@i
3. f : I {}\mrightarrow{}\mBbbR{}@i
4. f' : I {}\mrightarrow{}\mBbbR{}@i
5. g : J {}\mrightarrow{}\mBbbR{}@i
6. g' : J {}\mrightarrow{}\mBbbR{}@i
7. f[x] continuous for x \mmember{} I@i
8. f'[x] continuous for x \mmember{} I@i
9. g'[x] continuous for x \mmember{} J@i
10. \mlambda{}x.g'[x] = d(g[x])/dx on J@i
11. k : \mBbbN{}\msupplus{}@i
12. n : \{n:\mBbbN{}\msupplus{}| icompact(i-approx(I;n))\} @i
13. m : \{m:\mBbbN{}\msupplus{}| icompact(i-approx(J;m))\} @i
14. \mforall{}x:\{x:\mBbbR{}| x \mmember{} i-approx(I;n)\} . (f[x] \mmember{} i-approx(J;m))@i
15. mc1 : f'[x] continuous for x \mmember{} i-approx(I;n)
16. \mexists{}a:\mBbbR{}. \mforall{}[x:\{r:\mBbbR{}| r \mmember{} i-approx(I;n)\} ]. (|f'[x]| \mleq{} a)
17. mc2 : g'[x] continuous for x \mmember{} i-approx(J;m)
18. \mexists{}b:\mBbbR{}. \mforall{}[x:\{r:\mBbbR{}| r \mmember{} i-approx(J;m)\} ]. (|g'[x]| \mleq{} b)
19. f' \mmember{} i-approx(I;n) {}\mrightarrow{}\mBbbR{}
20. A : \mBbbN{}\msupplus{}
21. \mforall{}r:\mBbbR{}. ((r \mmember{} i-approx(I;n)) {}\mRightarrow{} (|f'[r]| \mleq{} (r(A)/r(2 * k))))
22. g \mmember{} i-approx(J;m) {}\mrightarrow{}\mBbbR{}
23. g' \mmember{} i-approx(J;m) {}\mrightarrow{}\mBbbR{}
24. f \mmember{} i-approx(I;n) {}\mrightarrow{}\mBbbR{}
25. d : \mBbbR{}
26. r0 < d
27. \mforall{}x,y:\mBbbR{}.
((x \mmember{} i-approx(I;n))
{}\mRightarrow{} (y \mmember{} i-approx(I;n))
{}\mRightarrow{} (|y - x| \mleq{} d)
{}\mRightarrow{} (|g[f[y]] - g[f[x]] - g'[f[x]] * (f[y] - f[x])| \mleq{} ((r1/r(A)) * |f[y] - f[x]|)))
28. B : \mBbbN{}\msupplus{}
29. \mforall{}r:\mBbbR{}. ((r \mmember{} i-approx(J;m)) {}\mRightarrow{} (((r1/r(A)) + |g'[r]|) \mleq{} (r(B)/r(2 * k))))
30. del : \mBbbR{}@i
31. r0 < del@i
32. \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] - f'[x] * (y - x)| \mleq{} ((r1/r(B)) * |y - x|)))@i
33. r0 < rmin(d;del)
34. x : \mBbbR{}@i
35. y : \mBbbR{}@i
36. x \mmember{} i-approx(I;n)@i
37. y \mmember{} i-approx(I;n)@i
38. |y - x| \mleq{} rmin(d;del)@i
\mvdash{} |g[f[y]] - g[f[x]] - (g'[f[x]] * f'[x]) * (y - x)| \mleq{} ((r1/r(k)) * |y - x|)
By
Latex:
((Assert (|y - x| \mleq{} d) \mwedge{} (|y - x| \mleq{} del) BY
(RWO "-1" 0 THEN Auto))
THEN D -1
THEN RepeatFor 2 (\mforall{}h:hyp. (FHyp h [-2] THENA Auto) ))
Home
Index