---

Step * of Lemma chain-rule_1

∀I,J:Interval. ∀f,f':I ⟶ℝ. ∀g,g':J ⟶ℝ.
  (maps-compact(I;J;x.f[x])
  ⇒ f[x] continuous for x ∈ I
  ⇒ f'[x] continuous for x ∈ I
  ⇒ g'[x] continuous for x ∈ J
  ⇒ λx.f'[x] = d(f[x])/dx on I
  ⇒ λx.g'[x] = d(g[x])/dx on J
  ⇒ λx.g'[f[x]] * f'[x] = d(g[f[x]])/dx on I)
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN (With ⌜n⌝ (D 7)⋅ THENA Auto)
   THEN D -1
   THEN ((InstLemma `continuous_functionality_wrt_subinterval` [⌜I⌝;⌜f'⌝;⌜i-approx(I;n)⌝] ⋅ THENA Auto)
         THEN (RenameVar `mc1' (-1)
               THEN (Assert ∃a:ℝ. ∀[x:{r:ℝ| r ∈ i-approx(I;n)} ]. (|f'[x]| ≤ a) BY
                           ((InstLemma `Inorm-bound` [⌜i-approx(I;n)⌝;⌜f'⌝;⌜mc1⌝]⋅ THENA Try (QuickAuto))
                            THEN (InstLemma `Inorm_wf` [⌜i-approx(I;n)⌝;⌜f'⌝;⌜mc1⌝]⋅ THENA Auto)
                            THEN With ⌜||f'[x]||_i-approx(I;n)⌝ (D 0)⋅
                            THEN Auto
                            THEN FLemma `i-member-approx` [-1]
                            THEN Auto))
               )⋅
         )
   THEN ((InstLemma `continuous_functionality_wrt_subinterval` [⌜J⌝;⌜g'⌝;⌜i-approx(J;m)⌝] ⋅ THENA Auto)
         THEN (RenameVar `mc2' (-1)
               THEN (Assert ∃b:ℝ. ∀[x:{r:ℝ| r ∈ i-approx(J;m)} ]. (|g'[x]| ≤ b) BY
                           ((InstLemma `Inorm-bound` [⌜i-approx(J;m)⌝;⌜g'⌝;⌜mc2⌝]⋅ THENA Try (QuickAuto))
                            THEN (InstLemma `Inorm_wf` [⌜i-approx(J;m)⌝;⌜g'⌝;⌜mc2⌝]⋅ THENA Auto)
                            THEN With ⌜||g'[x]||_i-approx(J;m)⌝ (D 0)⋅
                            THEN Auto
                            THEN FLemma `i-member-approx` [-1]
                            THEN 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.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|)))))}

---

Latex:

---

Latex:
\mforall{}I,J:Interval.  \mforall{}f,f':I  {}\mrightarrow{}\mBbbR{}.  \mforall{}g,g':J  {}\mrightarrow{}\mBbbR{}.
    (maps-compact(I;J;x.f[x])
    {}\mRightarrow{}  f[x]  continuous  for  x  \mmember{}  I
    {}\mRightarrow{}  f'[x]  continuous  for  x  \mmember{}  I
    {}\mRightarrow{}  g'[x]  continuous  for  x  \mmember{}  J
    {}\mRightarrow{}  \mlambda{}x.f'[x]  =  d(f[x])/dx  on  I
    {}\mRightarrow{}  \mlambda{}x.g'[x]  =  d(g[x])/dx  on  J
    {}\mRightarrow{}  \mlambda{}x.g'[f[x]]  *  f'[x]  =  d(g[f[x]])/dx  on  I)


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  (With  \mkleeneopen{}n\mkleeneclose{}  (D  7)\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  ((InstLemma  `continuous\_functionality\_wrt\_subinterval`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}f'\mkleeneclose{};\mkleeneopen{}i-approx(I;n)\mkleeneclose{}]  \mcdot{}
                THENA  Auto
                )
              THEN  (RenameVar  `mc1'  (-1)
                          THEN  (Assert  \mexists{}a:\mBbbR{}.  \mforall{}[x:\{r:\mBbbR{}|  r  \mmember{}  i-approx(I;n)\}  ].  (|f'[x]|  \mleq{}  a)  BY
                                                  ((InstLemma  `Inorm-bound`  [\mkleeneopen{}i-approx(I;n)\mkleeneclose{};\mkleeneopen{}f'\mkleeneclose{};\mkleeneopen{}mc1\mkleeneclose{}]\mcdot{}
                                                      THENA  Try  (QuickAuto)
                                                      )
                                                    THEN  (InstLemma  `Inorm\_wf`  [\mkleeneopen{}i-approx(I;n)\mkleeneclose{};\mkleeneopen{}f'\mkleeneclose{};\mkleeneopen{}mc1\mkleeneclose{}]\mcdot{}  THENA  Auto)
                                                    THEN  With  \mkleeneopen{}||f'[x]||\_i-approx(I;n)\mkleeneclose{}  (D  0)\mcdot{}
                                                    THEN  Auto
                                                    THEN  FLemma  `i-member-approx`  [-1]
                                                    THEN  Auto))
                          )\mcdot{}
              )
  THEN  ((InstLemma  `continuous\_functionality\_wrt\_subinterval`  [\mkleeneopen{}J\mkleeneclose{};\mkleeneopen{}g'\mkleeneclose{};\mkleeneopen{}i-approx(J;m)\mkleeneclose{}]  \mcdot{}
                THENA  Auto
                )
              THEN  (RenameVar  `mc2'  (-1)
                          THEN  (Assert  \mexists{}b:\mBbbR{}.  \mforall{}[x:\{r:\mBbbR{}|  r  \mmember{}  i-approx(J;m)\}  ].  (|g'[x]|  \mleq{}  b)  BY
                                                  ((InstLemma  `Inorm-bound`  [\mkleeneopen{}i-approx(J;m)\mkleeneclose{};\mkleeneopen{}g'\mkleeneclose{};\mkleeneopen{}mc2\mkleeneclose{}]\mcdot{}
                                                      THENA  Try  (QuickAuto)
                                                      )
                                                    THEN  (InstLemma  `Inorm\_wf`  [\mkleeneopen{}i-approx(J;m)\mkleeneclose{};\mkleeneopen{}g'\mkleeneclose{};\mkleeneopen{}mc2\mkleeneclose{}]\mcdot{}  THENA  Auto)
                                                    THEN  With  \mkleeneopen{}||g'[x]||\_i-approx(J;m)\mkleeneclose{}  (D  0)\mcdot{}
                                                    THEN  Auto
                                                    THEN  FLemma  `i-member-approx`  [-1]
                                                    THEN  Auto))
                          )\mcdot{}
              )\mcdot{})

---

Home Index