---

Step * 1 of Lemma chain-rule_0


1. I : Interval
2. J : Interval
3. f : I ⟶ℝ
4. f' : I ⟶ℝ
5. g : J ⟶ℝ
6. g' : J ⟶ℝ
7. maps-compact-proper(I;J;x.f[x])
8. f[x] (proper)continuous for x ∈ I
9. f'[x] (proper)continuous for x ∈ I
10. g'[x] (proper)continuous for x ∈ J
11. d(f[x])/dx = λx.f'[x] on I
12. d(g[x])/dx = λx.g'[x] on J
⊢ d(g[f[x]])/dx = λx.g'[f[x]] * f'[x] on I
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN (With ⌜n⌝ (D 7)⋅ THENA Auto)
   THEN D -1
   THEN (Assert iproper(i-approx(I;n)) BY
               (DVar `n' THEN (Unhide THEN Auto) THEN Unfold `iproper` 0 THEN Auto))
   THEN (InstLemma `proper-continuous-implies` [⌜I⌝;⌜f'⌝;⌜n⌝] ⋅ THENA Auto)
   THEN RenameVar `mc1' (-1)) }

1
1. I : Interval
2. J : Interval
3. f : I ⟶ℝ
4. f' : I ⟶ℝ
5. g : J ⟶ℝ
6. g' : J ⟶ℝ
7. f[x] (proper)continuous for x ∈ I
8. f'[x] (proper)continuous for x ∈ I
9. g'[x] (proper)continuous for x ∈ J
10. d(f[x])/dx = λx.f'[x] on I
11. d(g[x])/dx = λx.g'[x] on J
12. k : ℕ+
13. n : {n:ℕ+| icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))} 
14. m : {m:ℕ+| icompact(i-approx(J;m)) ∧ iproper(i-approx(J;m))} 
15. ∀x:{x:ℝ| x ∈ i-approx(I;n)} . (f[x] ∈ i-approx(J;m))
16. iproper(i-approx(I;n))
17. mc1 : f'[x] continuous for x ∈ i-approx(I;n)
⊢ ∃del:ℝ [((r0 < del)
         ∧ (∀x,y:ℝ.
              ((x ∈ i-approx(I;n))
              ⇒ (y ∈ i-approx(I;n))
              ⇒ (|y - x| ≤ del)
              ⇒ (|g[f[y]] - g[f[x]] - (g'[f[x]] * f'[x]) * (y - x)| ≤ ((r1/r(k)) * |y - x|)))))]

---

Latex:

---

Latex:

1.  I  :  Interval
2.  J  :  Interval
3.  f  :  I  {}\mrightarrow{}\mBbbR{}
4.  f'  :  I  {}\mrightarrow{}\mBbbR{}
5.  g  :  J  {}\mrightarrow{}\mBbbR{}
6.  g'  :  J  {}\mrightarrow{}\mBbbR{}
7.  maps-compact-proper(I;J;x.f[x])
8.  f[x]  (proper)continuous  for  x  \mmember{}  I
9.  f'[x]  (proper)continuous  for  x  \mmember{}  I
10.  g'[x]  (proper)continuous  for  x  \mmember{}  J
11.  d(f[x])/dx  =  \mlambda{}x.f'[x]  on  I
12.  d(g[x])/dx  =  \mlambda{}x.g'[x]  on  J
\mvdash{}  d(g[f[x]])/dx  =  \mlambda{}x.g'[f[x]]  *  f'[x]  on  I


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (With  \mkleeneopen{}n\mkleeneclose{}  (D  7)\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  (Assert  iproper(i-approx(I;n))  BY
                          (DVar  `n'  THEN  (Unhide  THEN  Auto)  THEN  Unfold  `iproper`  0  THEN  Auto))
  THEN  (InstLemma  `proper-continuous-implies`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}f'\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]  \mcdot{}  THENA  Auto)
  THEN  RenameVar  `mc1'  (-1))

---

Home Index