Step
*
1
1
of Lemma
cosine0
.....assertion.....
1. Σi.-1^i * (r0^2 * i)/(2 * i)! = cosine(r0)
⊢ Σi.-1^i * (r0^2 * i)/(2 * i)! = r1
BY
{ (Assert ⌜Σi.if (i =z 0) then r1 else r0 fi = r1⌝⋅ THENA Auto) }
1
1. Σi.-1^i * (r0^2 * i)/(2 * i)! = cosine(r0)
2. Σi.if (i =z 0) then r1 else r0 fi = r1
⊢ Σi.-1^i * (r0^2 * i)/(2 * i)! = r1
Latex:
Latex:
.....assertion.....
1. \mSigma{}i.-1\^{}i * (r0\^{}2 * i)/(2 * i)! = cosine(r0)
\mvdash{} \mSigma{}i.-1\^{}i * (r0\^{}2 * i)/(2 * i)! = r1
By
Latex:
(Assert \mkleeneopen{}\mSigma{}i.if (i =\msubz{} 0) then r1 else r0 fi = r1\mkleeneclose{}\mcdot{} THENA Auto)
Home
Index