Step
*
2
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. n : ℕ
3. i : ℕn + 1
⊢ d(x^2 * i)/dx = λx.if (i =z 0) then r0 else r(2 * i) * x^(2 * i) - 1 fi on (-∞, ∞)
BY
{ AutoSplit }
1
1. lim n→∞.Σ{-1^i * (x^2 * i)/(2 * i)! | 0≤i≤n} = λx.cosine(x) for x ∈ (-∞, ∞)
2. n : ℕ
3. i : ℕn + 1
4. i = 0 ∈ ℤ
⊢ d(x@0^2 * i)/dx@0 = λx@0.r0 on (-∞, ∞)
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. n : \mBbbN{}
3. i : \mBbbN{}n + 1
\mvdash{} d(x\^{}2 * i)/dx = \mlambda{}x.if (i =\msubz{} 0) then r0 else r(2 * i) * x\^{}(2 * i) - 1 fi on (-\minfty{}, \minfty{})
By
Latex:
AutoSplit
Home
Index