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. : ℕ@i
2. {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