---

Step * 2 1 2 1 of Lemma small-rexp-remainder


1. x : {x:ℝ| |x| ≤ (r1/r(4))} 
2. n : ℕ
3. ¬(n = 0 ∈ ℤ)
4. e : {e:ℝ| r0 < e} 
5. c : ℝ
6. rmin(r0;x) ≤ c
7. c ≤ rmax(r0;x)
8. |Taylor-remainder((-∞, ∞);n;x;r0;k,x.e^x) - (x - c^n * (e^c/r((n)!))) * (x - r0)| ≤ e
9. (e^x - Σ{(x^k/r((k)!)) | 0≤k≤n}) = Taylor-remainder((-∞, ∞);n;x;r0;k,x.e^x)
10. r0 < r(4^n * 3 * (n)!)
⊢ |e^x - Σ{(x^k/r((k)!)) | 0≤k≤n}| ≤ ((r1/r(4^n * 3 * (n)!)) + e)
BY
{ (RepeatFor 2 (MoveToConcl (-2))
   THEN GenConclTerms  Auto [⌜Taylor-remainder((-∞, ∞);n;x;r0;k,x.e^x)⌝;⌜e^x - Σ{(x^k/r((k)!)) | 0≤k≤n}⌝]⋅
   ) }

1
1. x : {x:ℝ| |x| ≤ (r1/r(4))} 
2. n : ℕ
3. ¬(n = 0 ∈ ℤ)
4. e : {e:ℝ| r0 < e} 
5. c : ℝ
6. rmin(r0;x) ≤ c
7. c ≤ rmax(r0;x)
8. r0 < r(4^n * 3 * (n)!)
9. v : ℝ
10. Taylor-remainder((-∞, ∞);n;x;r0;k,x.e^x) = v ∈ ℝ
11. v1 : ℝ
12. (e^x - Σ{(x^k/r((k)!)) | 0≤k≤n}) = v1 ∈ ℝ
⊢ (|v - (x - c^n * (e^c/r((n)!))) * (x - r0)| ≤ e) ⇒ (v1 = v) ⇒ (|v1| ≤ ((r1/r(4^n * 3 * (n)!)) + e))

---

Latex:

---

Latex:

1.  x  :  \{x:\mBbbR{}|  |x|  \mleq{}  (r1/r(4))\} 
2.  n  :  \mBbbN{}
3.  \mneg{}(n  =  0)
4.  e  :  \{e:\mBbbR{}|  r0  <  e\} 
5.  c  :  \mBbbR{}
6.  rmin(r0;x)  \mleq{}  c
7.  c  \mleq{}  rmax(r0;x)
8.  |Taylor-remainder((-\minfty{},  \minfty{});n;x;r0;k,x.e\^{}x)  -  (x  -  c\^{}n  *  (e\^{}c/r((n)!)))  *  (x  -  r0)|  \mleq{}  e
9.  (e\^{}x  -  \mSigma{}\{(x\^{}k/r((k)!))  |  0\mleq{}k\mleq{}n\})  =  Taylor-remainder((-\minfty{},  \minfty{});n;x;r0;k,x.e\^{}x)
10.  r0  <  r(4\^{}n  *  3  *  (n)!)
\mvdash{}  |e\^{}x  -  \mSigma{}\{(x\^{}k/r((k)!))  |  0\mleq{}k\mleq{}n\}|  \mleq{}  ((r1/r(4\^{}n  *  3  *  (n)!))  +  e)


By

---

Latex:
(RepeatFor  2  (MoveToConcl  (-2))
  THEN  GenConclTerms    Auto  [\mkleeneopen{}Taylor-remainder((-\minfty{},  \minfty{});n;x;r0;k,x.e\^{}x)\mkleeneclose{};
            \mkleeneopen{}e\^{}x  -  \mSigma{}\{(x\^{}k/r((k)!))  |  0\mleq{}k\mleq{}n\}\mkleeneclose{}]\mcdot{}
  )

---

Home Index