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