---

Step * 1 of Lemma fun-converges-to-cosine


1. ∀x:ℝ. Σi.-1^i * (x^2 * i)/(2 * i)! = cosine(x)
⊢ lim n→∞.Σ{-1^i * (x^2 * i)/(2 * i)! | 0≤i≤n} = λx.cosine(x) for x ∈ (-∞, ∞)
BY
{ (InstLemma `fun-series-converges-to-everywhere` [⌜λ2i x.-1^i * (x^2 * i)/(2 * i)!⌝;⌜λ2x.cosine(x)⌝]⋅
   THEN Auto
   THEN D 0 With ⌜(r1/r(4))⌝ 
   THEN Auto
   THEN Try ((nRMul ⌜r(4)⌝ 0⋅ THEN Auto))) }

1
1. ∀x:ℝ. Σi.-1^i * (x^2 * i)/(2 * i)! = cosine(x)
2. m : ℕ+
3. r0 ≤ (r1/r(4))
4. (r1/r(4)) < r1
⊢ ∃N:ℕ
   ∀n:{N...}. ∀x:{x:ℝ| |x| ≤ r(m)} .
     (|-1^n + 1 * (x^2 * (n + 1))/(2 * (n + 1))!| ≤ ((r1/r(4)) * |-1^n * (x^2 * n)/(2 * n)!|))

---

Latex:

---

Latex:

1.  \mforall{}x:\mBbbR{}.  \mSigma{}i.-1\^{}i  *  (x\^{}2  *  i)/(2  *  i)!  =  cosine(x)
\mvdash{}  lim  n\mrightarrow{}\minfty{}.\mSigma{}\{-1\^{}i  *  (x\^{}2  *  i)/(2  *  i)!  |  0\mleq{}i\mleq{}n\}  =  \mlambda{}x.cosine(x)  for  x  \mmember{}  (-\minfty{},  \minfty{})


By

---

Latex:
(InstLemma  `fun-series-converges-to-everywhere`  [\mkleeneopen{}\mlambda{}\msubtwo{}i  x.-1\^{}i  *  (x\^{}2  *  i)/(2  *  i)!\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.cosine(x)\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  D  0  With  \mkleeneopen{}(r1/r(4))\mkleeneclose{} 
  THEN  Auto
  THEN  Try  ((nRMul  \mkleeneopen{}r(4)\mkleeneclose{}  0\mcdot{}  THEN  Auto)))

---

Home Index