Step
*
1
1
1
2
of Lemma
cosine0
1. Σi.-1^i * (r0^2 * i)/(2 * i)! = cosine(r0)
2. i : {1...}
⊢ r0 = -1^i * (r0^2 * i)/(2 * i)!
BY
{ (RWO "rnexp0" 0 THEN Auto THEN (RWW "int-rmul-req int-rdiv-req" 0 THENM nRNorm 0) THEN Auto) }
Latex:
Latex:
1. \mSigma{}i.-1\^{}i * (r0\^{}2 * i)/(2 * i)! = cosine(r0)
2. i : \{1...\}
\mvdash{} r0 = -1\^{}i * (r0\^{}2 * i)/(2 * i)!
By
Latex:
(RWO "rnexp0" 0 THEN Auto THEN (RWW "int-rmul-req int-rdiv-req" 0 THENM nRNorm 0) THEN Auto)
Home
Index