---

Step * of Lemma derivative-sine

d(sine(x))/dx = λx.cosine(x) on (-∞, ∞)
BY
{ (InstLemma `fun-converges-to-sine` []
   THEN InstLemma `fun-converges-to-derivative` [⌜(-∞, ∞)⌝;⌜λ2n x.Σ{-1^i * (x^(2 * i) + 1)/((2 * i) + 1)! | 0≤i≤n}⌝;
   ⌜λ2n x.Σ{-1^i * (x^2 * i)/(2 * i)! | 0≤i≤n}⌝;⌜λ2x.sine(x)⌝;⌜λ2x.cosine(x)⌝]⋅
   THEN Auto
   THEN ProveDerivative
   THEN Auto) }

1
1. lim n→∞.Σ{-1^i * (x^(2 * i) + 1)/((2 * i) + 1)! | 0≤i≤n} = λx.sine(x) for x ∈ (-∞, ∞)
2. n : ℕ
3. i : ℕn + 1
⊢ d((x^(2 * i) + 1)/((2 * i) + 1)!)/dx = λx.(x^2 * i)/(2 * i)! on (-∞, ∞)

---

Latex:

---

Latex:
d(sine(x))/dx  =  \mlambda{}x.cosine(x)  on  (-\minfty{},  \minfty{})


By

---

Latex:
(InstLemma  `fun-converges-to-sine`  []
  THEN  InstLemma  `fun-converges-to-derivative`  [\mkleeneopen{}(-\minfty{},  \minfty{})\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}n  x.\mSigma{}\{-1\^{}i  *  (x\^{}(2  *  i)  +  1)/((2  *  i)
                                                                                                                    +  1)!  |  0\mleq{}i\mleq{}n\}\mkleeneclose{};
  \mkleeneopen{}\mlambda{}\msubtwo{}n  x.\mSigma{}\{-1\^{}i  *  (x\^{}2  *  i)/(2  *  i)!  |  0\mleq{}i\mleq{}n\}\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.sine(x)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.cosine(x)\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  ProveDerivative
  THEN  Auto)

---

Home Index