Step
*
3
of Lemma
fun-converges-to-rexp
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 ∈ (-∞, ∞)
BY
{ (MoveToConcl (-1) THEN BLemma `fun-converges-to_functionality` THEN Auto) }
1
1. n : ℕ@i
2. x : {x:ℝ| x ∈ (-∞, ∞)} @i
⊢ Σ{(r1/r((i)!)) * x^i | 0≤i≤n} = Σ{(x^i)/(i)! | 0≤i≤n}
Latex:
Latex:
1.  lim  n\mrightarrow{}\minfty{}.\mSigma{}\{(r1/r((i)!))  *  x\^{}i  |  0\mleq{}i\mleq{}n\}  =  \mlambda{}x.e\^{}x  for  x  \mmember{}  (-\minfty{},  \minfty{})
\mvdash{}  lim  n\mrightarrow{}\minfty{}.\mSigma{}\{(x\^{}i)/(i)!  |  0\mleq{}i\mleq{}n\}  =  \mlambda{}x.e\^{}x  for  x  \mmember{}  (-\minfty{},  \minfty{})
By
Latex:
(MoveToConcl  (-1)  THEN  BLemma  `fun-converges-to\_functionality`  THEN  Auto)
Home
Index