---

Step * 3 1 1 of Lemma fun-converges-to-rexp


1. n : ℕ@i
2. x : {x:ℝ| x ∈ (-∞, ∞)} @i
3. i : ℤ@i
4. 0 ≤ i
5. i ≤ n
⊢ ((r1/r((i)!)) * x^i) = (x^i)/(i)!
BY
{ ((RWO "int-rdiv-req" 0 THEN Auto) THEN nRMul ⌜r((i)!)⌝ 0⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}@i
2.  x  :  \{x:\mBbbR{}|  x  \mmember{}  (-\minfty{},  \minfty{})\}  @i
3.  i  :  \mBbbZ{}@i
4.  0  \mleq{}  i
5.  i  \mleq{}  n
\mvdash{}  ((r1/r((i)!))  *  x\^{}i)  =  (x\^{}i)/(i)!


By

---

Latex:
((RWO  "int-rdiv-req"  0  THEN  Auto)  THEN  nRMul  \mkleeneopen{}r((i)!)\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index