---

Step * of Lemma trivial-Taylor-approx

∀[I:Interval]. ∀[n:ℕ]. ∀[F:ℕn + 1 ⟶ I ⟶ℝ]. ∀[a,b:{x:ℝ| x ∈ I} ].
  ((a = b) ⇒ (Taylor-approx(n;a;b;i,x.F[i;x]) = F[0;a]))
BY
{ (Auto
   THEN Unfold `Taylor-approx` 0
   THEN RWO "rsum-split-first" 0
   THEN Auto
   THEN (Assert ⌜Σ{(F[k;a]/r((k)!)) * b - a^k | 0 + 1≤k≤n} = Σ{r0 | 0 + 1≤k≤n}⌝⋅
   THENM ((RWW "-1 rsum-zero" 0 THENA Auto) THEN Reduce 0 THEN nRNorm 0 THEN Auto)
   )) }

1
.....assertion..... 
1. I : Interval
2. n : ℕ
3. F : ℕn + 1 ⟶ I ⟶ℝ
4. a : {x:ℝ| x ∈ I} 
5. b : {x:ℝ| x ∈ I} 
6. a = b
⊢ Σ{(F[k;a]/r((k)!)) * b - a^k | 0 + 1≤k≤n} = Σ{r0 | 0 + 1≤k≤n}

---

Latex:

---

Latex:
\mforall{}[I:Interval].  \mforall{}[n:\mBbbN{}].  \mforall{}[F:\mBbbN{}n  +  1  {}\mrightarrow{}  I  {}\mrightarrow{}\mBbbR{}].  \mforall{}[a,b:\{x:\mBbbR{}|  x  \mmember{}  I\}  ].
    ((a  =  b)  {}\mRightarrow{}  (Taylor-approx(n;a;b;i,x.F[i;x])  =  F[0;a]))


By

---

Latex:
(Auto
  THEN  Unfold  `Taylor-approx`  0
  THEN  RWO  "rsum-split-first"  0
  THEN  Auto
  THEN  (Assert  \mkleeneopen{}\mSigma{}\{(F[k;a]/r((k)!))  *  b  -  a\^{}k  |  0  +  1\mleq{}k\mleq{}n\}  =  \mSigma{}\{r0  |  0  +  1\mleq{}k\mleq{}n\}\mkleeneclose{}\mcdot{}
  THENM  ((RWW  "-1  rsum-zero"  0  THENA  Auto)  THEN  Reduce  0  THEN  nRNorm  0  THEN  Auto)
  ))

---

Home Index