---

Step * 1 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.f'[x] = d(f[x])/dx on I@i
11. λx.g'[x] = d(g[x])/dx on J@i
12. k : ℕ+@i
13. n : {n:ℕ+| icompact(i-approx(I;n))} @i
14. m : {m:ℕ+| icompact(i-approx(J;m))} @i
15. ∀x:{x:ℝ| x ∈ i-approx(I;n)} . (f[x] ∈ i-approx(J;m))@i
16. mc1 : f'[x] continuous for x ∈ i-approx(I;n)
17. ∃a:ℝ. ∀[x:{r:ℝ| r ∈ i-approx(I;n)} ]. (|f'[x]| ≤ a)
18. mc2 : g'[x] continuous for x ∈ i-approx(J;m)
19. ∃b:ℝ. ∀[x:{r:ℝ| r ∈ i-approx(J;m)} ]. (|g'[x]| ≤ b)
⊢ ∃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|)))))}
BY
{ ((Assert f' ∈ i-approx(I;n) ⟶ℝ BY
          Auto)
   THEN (Assert ∃A:ℕ+. ∀r:ℝ. ((r ∈ i-approx(I;n)) ⇒ (|f'[r]| ≤ (r(A)/r(2 * k)))) BY
               (D -4
                THEN (InstLemma `r-bound-property` [⌜a⌝]⋅ THENA Auto)
                THEN With ⌜(2 * k) * r-bound(a)⌝ (D 0)⋅
                THEN Auto
                THEN RWO "18" 0
                THEN Auto
                THEN RWO "-3" 0
                THEN Auto))
   THEN D -1) }

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.f'[x] = d(f[x])/dx on I@i
11. λx.g'[x] = d(g[x])/dx on J@i
12. k : ℕ+@i
13. n : {n:ℕ+| icompact(i-approx(I;n))} @i
14. m : {m:ℕ+| icompact(i-approx(J;m))} @i
15. ∀x:{x:ℝ| x ∈ i-approx(I;n)} . (f[x] ∈ i-approx(J;m))@i
16. mc1 : f'[x] continuous for x ∈ i-approx(I;n)
17. ∃a:ℝ. ∀[x:{r:ℝ| r ∈ i-approx(I;n)} ]. (|f'[x]| ≤ a)
18. mc2 : g'[x] continuous for x ∈ i-approx(J;m)
19. ∃b:ℝ. ∀[x:{r:ℝ| r ∈ i-approx(J;m)} ]. (|g'[x]| ≤ b)
20. f' ∈ i-approx(I;n) ⟶ℝ
21. A : ℕ+
22. ∀r:ℝ. ((r ∈ i-approx(I;n)) ⇒ (|f'[r]| ≤ (r(A)/r(2 * k))))
⊢ ∃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@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.f'[x]  =  d(f[x])/dx  on  I@i
11.  \mlambda{}x.g'[x]  =  d(g[x])/dx  on  J@i
12.  k  :  \mBbbN{}\msupplus{}@i
13.  n  :  \{n:\mBbbN{}\msupplus{}|  icompact(i-approx(I;n))\}  @i
14.  m  :  \{m:\mBbbN{}\msupplus{}|  icompact(i-approx(J;m))\}  @i
15.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  i-approx(I;n)\}  .  (f[x]  \mmember{}  i-approx(J;m))@i
16.  mc1  :  f'[x]  continuous  for  x  \mmember{}  i-approx(I;n)
17.  \mexists{}a:\mBbbR{}.  \mforall{}[x:\{r:\mBbbR{}|  r  \mmember{}  i-approx(I;n)\}  ].  (|f'[x]|  \mleq{}  a)
18.  mc2  :  g'[x]  continuous  for  x  \mmember{}  i-approx(J;m)
19.  \mexists{}b:\mBbbR{}.  \mforall{}[x:\{r:\mBbbR{}|  r  \mmember{}  i-approx(J;m)\}  ].  (|g'[x]|  \mleq{}  b)
\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{}  (|g[f[y]]  -  g[f[x]]  -  (g'[f[x]]  *  f'[x])  *  (y  -  x)|  \mleq{}  ((r1/r(k))  *  |y  -  x|)))))\}


By

---

Latex:
((Assert  f'  \mmember{}  i-approx(I;n)  {}\mrightarrow{}\mBbbR{}  BY
                Auto)
  THEN  (Assert  \mexists{}A:\mBbbN{}\msupplus{}.  \mforall{}r:\mBbbR{}.  ((r  \mmember{}  i-approx(I;n))  {}\mRightarrow{}  (|f'[r]|  \mleq{}  (r(A)/r(2  *  k))))  BY
                          (D  -4
                            THEN  (InstLemma  `r-bound-property`  [\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  With  \mkleeneopen{}(2  *  k)  *  r-bound(a)\mkleeneclose{}  (D  0)\mcdot{}
                            THEN  Auto
                            THEN  RWO  "18"  0
                            THEN  Auto
                            THEN  RWO  "-3"  0
                            THEN  Auto))
  THEN  D  -1)

---

Home Index