---

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


1. n : ℕ@i
2. x : {x:ℝ| x ∈ (-∞, ∞)} @i
⊢ Σ{(r1/r((i)!)) * x^i | 0≤i≤n} = Σ{(x^i)/(i)! | 0≤i≤n}
BY
{ ((BLemma `rsum_functionality` THEN Auto) THEN D 0 THEN Auto) }

1
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)!

---

Latex:

---

Latex:

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


By

---

Latex:
((BLemma  `rsum\_functionality`  THEN  Auto)  THEN  D  0  THEN  Auto)

---

Home Index