---

Step * of Lemma derivative-cosine

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

1
.....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 ∈ (-∞, ∞)

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

---

Latex:

---

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


By

---

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

---

Home Index