Step
*
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)/((2 * i) + 1)!
BY
{ (RWO "rnexp0" 0 THEN Auto) }
1
1. Σi.-1^i * (r0^(2 * i) + 1)/((2 * i) + 1)! = sine(r0)
2. i : ℕ
⊢ r0 = -1^i * (r0)/((2 * i) + 1)!
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)/((2 * i) + 1)!
By
Latex:
(RWO "rnexp0" 0 THEN Auto)
Home
Index