---

Step * 2 1 of Lemma Taylor-theorem-for-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))
           ∧ (|f[b] - Σ{([f[a]; g[a]; h[a]][k]/r((k)!)) * b - a^k | 0≤k≤1} - (b - c^1 * (h[c]/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))
BY
{ (Assert Σ{([f[a]; g[a]; h[a]][k]/r((k)!)) * b - a^k | 0≤k≤1} = (f[a] + (g[a] * (b - a))) BY
         (RWO "rsum_unroll" 0 THENA Auto)) }

1
.....aux..... 
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))
           ∧ (|f[b] - Σ{([f[a]; g[a]; h[a]][k]/r((k)!)) * b - a^k | 0≤k≤1} - (b - c^1 * (h[c]/r((1)!)))
             * (b - a)| ≤ e))))
⊢ if 1 <z 0 then r0
if (1 =z 0) then ([f[a]; g[a]; h[a]][0]/r((0)!)) * b - a^0
else Σ{([f[a]; g[a]; h[a]][k]/r((k)!)) * b - a^k | 0≤k≤1 - 1} + (([f[a]; g[a]; h[a]][1]/r((1)!)) * b - a^1)
fi 
= (f[a] + (g[a] * (b - a)))

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))
           ∧ (|f[b] - Σ{([f[a]; g[a]; h[a]][k]/r((k)!)) * b - a^k | 0≤k≤1} - (b - c^1 * (h[c]/r((1)!)))
             * (b - a)| ≤ e))))
14. Σ{([f[a]; g[a]; h[a]][k]/r((k)!)) * b - a^k | 0≤k≤1} = (f[a] + (g[a] * (b - a)))
⊢ ∃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:

1.  I  :  Interval
2.  iproper(I)
3.  f  :  I  {}\mrightarrow{}\mBbbR{}
4.  g  :  I  {}\mrightarrow{}\mBbbR{}
5.  h  :  I  {}\mrightarrow{}\mBbbR{}
6.  \mforall{}x,y:\{a:\mBbbR{}|  a  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (h[x]  =  h[y]))
7.  d(f[x])/dx  =  \mlambda{}x.g[x]  on  I
8.  d(g[x])/dx  =  \mlambda{}x.h[x]  on  I
9.  a  :  \{a:\mBbbR{}|  a  \mmember{}  I\} 
10.  b  :  \{a:\mBbbR{}|  a  \mmember{}  I\} 
11.  e  :  \mBbbR{}
12.  r0  <  e
13.  \mforall{}e:\mBbbR{}
            ((r0  <  e)
            {}\mRightarrow{}  (\mexists{}c:\mBbbR{}
                      ((rmin(a;b)  \mleq{}  c)
                      \mwedge{}  (c  \mleq{}  rmax(a;b))
                      \mwedge{}  (|f[b]  -  \mSigma{}\{([f[a];  g[a];  h[a]][k]/r((k)!))  *  b  -  a\^{}k  |  0\mleq{}k\mleq{}1\}  -  (b  -  c\^{}1
                          *  (h[c]/r((1)!)))
                          *  (b  -  a)|  \mleq{}  e))))
\mvdash{}  \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:
(Assert  \mSigma{}\{([f[a];  g[a];  h[a]][k]/r((k)!))  *  b  -  a\^{}k  |  0\mleq{}k\mleq{}1\}  =  (f[a]  +  (g[a]  *  (b  -  a)))  BY
              (RWO  "rsum\_unroll"  0  THENA  Auto))

---

Home Index