---

Step * of Lemma fun-converges-to-rexp

No Annotations
lim n→∞.Σ{(x^i)/(i)! | 0≤i≤n} = λx.e^x for x ∈ (-∞, ∞)
BY
{ (InstLemma `power-series-converges-everywhere` [⌜λ2n.(r1/r((n)!))⌝;⌜λ2x.e^x⌝]⋅ THENA Auto) }

1
1. x : ℝ
⊢ Σi.(r1/r((i)!)) * x^i = e^x

2
1. r : {r:ℝ| r0 < r} 
⊢ ∃N:ℕ. ∀n:{N...}. (|(r1/r((n + 1)!))| ≤ (|(r1/r((n)!))|/r))

3
1. lim n→∞.Σ{(r1/r((i)!)) * x^i | 0≤i≤n} = λx.e^x for x ∈ (-∞, ∞)
⊢ lim n→∞.Σ{(x^i)/(i)! | 0≤i≤n} = λx.e^x for x ∈ (-∞, ∞)

---

Latex:

---

Latex:
No  Annotations
lim  n\mrightarrow{}\minfty{}.\mSigma{}\{(x\^{}i)/(i)!  |  0\mleq{}i\mleq{}n\}  =  \mlambda{}x.e\^{}x  for  x  \mmember{}  (-\minfty{},  \minfty{})


By

---

Latex:
(InstLemma  `power-series-converges-everywhere`  [\mkleeneopen{}\mlambda{}\msubtwo{}n.(r1/r((n)!))\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.e\^{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index