---

Step * 1 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
{ (RepeatFor 3 (ParallelLast)
   THEN ExRepD
   THEN (D 0 With ⌜N + 1⌝  THENA Auto)
   THEN ParallelLast
   THEN (D 0 THENA Auto)
   THEN BackThruSomeHyp) }

---

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:
(RepeatFor  3  (ParallelLast)
  THEN  ExRepD
  THEN  (D  0  With  \mkleeneopen{}N  +  1\mkleeneclose{}    THENA  Auto)
  THEN  ParallelLast
  THEN  (D  0  THENA  Auto)
  THEN  BackThruSomeHyp)

---

Home Index