---

Step * of Lemma Taylor-theorem-for-2

∀I:Interval
  (iproper(I)
  ⇒ (∀f,g,h:I ⟶ℝ.
        ((∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ (h[x] = h[y])))
        ⇒ d(f[x])/dx = λx.g[x] on I
        ⇒ d(g[x])/dx = λx.h[x] on I
        ⇒ (∀a,b:{a:ℝ| a ∈ I} . ∀e:ℝ.
              ((r0 < e)
              ⇒ (∃c:ℝ
                   ((rmin(a;b) ≤ c)
                   ∧ (c ≤ rmax(a;b))
                   ∧ (|f[b] - f[a] + (g[a] * (b - a)) - ((b - c) * h[c]) * (b - a)| ≤ e))))))))
BY
{ (Intros
   THEN (InstLemma `Taylor-theorem` [⌜I⌝;⌜1⌝;⌜λ2i x.[f[x]; g[x]; h[x]][i]⌝;⌜a⌝;⌜b⌝]⋅
         THENA (Auto THEN Try (((D 0 THENW Auto) THEN Reduce -1 THEN (IntSegCases (-1) THEN Reduce 0) THEN Trivial)))
         )
   ) }

1
1. I : Interval
2. iproper(I)
3. f : I ⟶ℝ
4. g : I ⟶ℝ
5. h : I ⟶ℝ
6. ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ (h[x] = h[y]))
7. d(f[x])/dx = λx.g[x] on I
8. d(g[x])/dx = λx.h[x] on I
9. a : {a:ℝ| a ∈ I} 
10. b : {a:ℝ| a ∈ I} 
11. e : ℝ
12. r0 < e
13. k : ℕ1 + 2
14. x : {a:ℝ| a ∈ I} 
15. y : {a:ℝ| a ∈ I} 
16. x = y
⊢ [f[x]; g[x]; h[x]][k] = [f[y]; g[y]; h[y]][k]

2
1. I : Interval
2. iproper(I)
3. f : I ⟶ℝ
4. g : I ⟶ℝ
5. h : I ⟶ℝ
6. ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ (h[x] = h[y]))
7. d(f[x])/dx = λx.g[x] on I
8. d(g[x])/dx = λx.h[x] on I
9. a : {a:ℝ| a ∈ I} 
10. b : {a:ℝ| a ∈ I} 
11. e : ℝ
12. r0 < e
13. ∀e:ℝ
      ((r0 < e)
      ⇒ (∃c:ℝ
           ((rmin(a;b) ≤ c)
           ∧ (c ≤ rmax(a;b))
           ∧ (|Taylor-remainder(I;1;b;a;k,x.[f[x]; g[x]; h[x]][k]) - (b - c^1 * ([f[c]; g[c]; h[c]][1 + 1]/r((1)!)))
             * (b - a)| ≤ e))))
⊢ ∃c:ℝ. ((rmin(a;b) ≤ c) ∧ (c ≤ rmax(a;b)) ∧ (|f[b] - f[a] + (g[a] * (b - a)) - ((b - c) * h[c]) * (b - a)| ≤ e))

---

Latex:

---

Latex:
\mforall{}I:Interval
    (iproper(I)
    {}\mRightarrow{}  (\mforall{}f,g,h:I  {}\mrightarrow{}\mBbbR{}.
                ((\mforall{}x,y:\{a:\mBbbR{}|  a  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (h[x]  =  h[y])))
                {}\mRightarrow{}  d(f[x])/dx  =  \mlambda{}x.g[x]  on  I
                {}\mRightarrow{}  d(g[x])/dx  =  \mlambda{}x.h[x]  on  I
                {}\mRightarrow{}  (\mforall{}a,b:\{a:\mBbbR{}|  a  \mmember{}  I\}  .  \mforall{}e:\mBbbR{}.
                            ((r0  <  e)
                            {}\mRightarrow{}  (\mexists{}c:\mBbbR{}
                                      ((rmin(a;b)  \mleq{}  c)
                                      \mwedge{}  (c  \mleq{}  rmax(a;b))
                                      \mwedge{}  (|f[b]  -  f[a]  +  (g[a]  *  (b  -  a))  -  ((b  -  c)  *  h[c])  *  (b  -  a)|  \mleq{}  e))))))))


By

---

Latex:
(Intros
  THEN  (InstLemma  `Taylor-theorem`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i  x.[f[x];  g[x];  h[x]][i]\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}
              THENA  (Auto
                            THEN  Try  (((D  0  THENW  Auto)
                                                  THEN  Reduce  -1
                                                  THEN  (IntSegCases  (-1)  THEN  Reduce  0)
                                                  THEN  Trivial))
                            )
              )
  )

---

Home Index