---

Step * 1 1 1 2 of Lemma rexp0


1. Σn.(r0^n)/(n)! = e^r0
2. i : {1...}
⊢ r0 = (r0^i)/(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{}n.(r0\^{}n)/(n)!  =  e\^{}r0
2.  i  :  \{1...\}
\mvdash{}  r0  =  (r0\^{}i)/(i)!


By

---

Latex:
(RWO  "rnexp0"  0  THEN  Auto  THEN  (RWW  "int-rmul-req  int-rdiv-req"  0  THENM  nRNorm  0)  THEN  Auto)

---

Home Index