---

Step * of Lemma sine0

sine(r0) = r0
BY
{ (Auto THEN (InstLemma `sine-is-limit` [⌜r0⌝]⋅ THENA Auto)) }

1
1. Σi.-1^i * (r0^(2 * i) + 1)/((2 * i) + 1)! = sine(r0)
⊢ sine(r0) = r0

---

Latex:

---

Latex:
sine(r0)  =  r0


By

---

Latex:
(Auto  THEN  (InstLemma  `sine-is-limit`  [\mkleeneopen{}r0\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index