Step
*
of Lemma
cosine-is-limit
∀x:ℝ. Σi.-1^i * (x^2 * i)/(2 * i)! = cosine(x)
BY
{ (Auto THEN Unfold `cosine` 0 THEN (GenConclAtAddr [2;1] THENA Auto) THEN D -2 THEN Reduce 0 THEN Auto) }
Latex:
Latex:
\mforall{}x:\mBbbR{}. \mSigma{}i.-1\^{}i * (x\^{}2 * i)/(2 * i)! = cosine(x)
By
Latex:
(Auto
THEN Unfold `cosine` 0
THEN (GenConclAtAddr [2;1] THENA Auto)
THEN D -2
THEN Reduce 0
THEN Auto)
Home
Index