---

Step * 1 1 of Lemma derivative-cosine


1. lim n→∞.Σ{-1^i * (x^2 * i)/(2 * i)! | 0≤i≤n} = λx.cosine(x) for x ∈ (-∞, ∞)
2. lim n→∞.Σ{-1^i * (x^(2 * i) + 1)/((2 * i) + 1)! | 0≤i≤n} = λx.sine(x) for x ∈ (-∞, ∞)
⊢ lim n→∞.-(Σ{-1^i * (x^(2 * i) + 1)/((2 * i) + 1)! | 0≤i≤n - 1}) = λy.-(sine(y)) for x ∈ (-∞, ∞)
BY
{ (BLemma `fun-converges-to-rminus` THEN Auto) }

1
1. lim n→∞.Σ{-1^i * (x^2 * i)/(2 * i)! | 0≤i≤n} = λx.cosine(x) for x ∈ (-∞, ∞)
2. lim n→∞.Σ{-1^i * (x^(2 * i) + 1)/((2 * i) + 1)! | 0≤i≤n} = λx.sine(x) for x ∈ (-∞, ∞)
⊢ lim n→∞.Σ{-1^i * (x^(2 * i) + 1)/((2 * i) + 1)! | 0≤i≤n - 1} = λy.sine(y) for x ∈ (-∞, ∞)

---

Latex:

---

Latex:

1.  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{})
2.  lim  n\mrightarrow{}\minfty{}.\mSigma{}\{-1\^{}i  *  (x\^{}(2  *  i)  +  1)/((2  *  i)  +  1)!  |  0\mleq{}i\mleq{}n\}  =  \mlambda{}x.sine(x)  for  x  \mmember{}  (-\minfty{},  \minfty{})
\mvdash{}  lim  n\mrightarrow{}\minfty{}.-(\mSigma{}\{-1\^{}i  *  (x\^{}(2  *  i)  +  1)/((2  *  i)  +  1)!  |  0\mleq{}i\mleq{}n  -  1\})  =  \mlambda{}y.-(sine(y))  for  x  \mmember{}  (-\minfty{},  \minfty{})


By

---

Latex:
(BLemma  `fun-converges-to-rminus`  THEN  Auto)

---

Home Index