---

Step * 1 of Lemma derivative-cosine

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

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:
.....antecedent..... 
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{})
\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:
InstLemma  `fun-converges-to-sine`  []

---

Home Index