# Metamath Proof Explorer

## Theorem efcvg

Description: The series that defines the exponential function converges to it. (Contributed by NM, 9-Jan-2006) (Revised by Mario Carneiro, 28-Apr-2014)

Ref Expression
Hypothesis efcvg.1 ${⊢}{F}=\left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}}}{{n}!}\right)$
Assertion efcvg ${⊢}{A}\in ℂ\to seq0\left(+,{F}\right)⇝{\mathrm{e}}^{{A}}$

### Proof

Step Hyp Ref Expression
1 efcvg.1 ${⊢}{F}=\left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}}}{{n}!}\right)$
2 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
3 0zd ${⊢}{A}\in ℂ\to 0\in ℤ$
4 1 eftval ${⊢}{k}\in {ℕ}_{0}\to {F}\left({k}\right)=\frac{{{A}}^{{k}}}{{k}!}$
5 4 adantl ${⊢}\left({A}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to {F}\left({k}\right)=\frac{{{A}}^{{k}}}{{k}!}$
6 eftcl ${⊢}\left({A}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to \frac{{{A}}^{{k}}}{{k}!}\in ℂ$
7 1 efcllem ${⊢}{A}\in ℂ\to seq0\left(+,{F}\right)\in \mathrm{dom}⇝$
8 2 3 5 6 7 isumclim2 ${⊢}{A}\in ℂ\to seq0\left(+,{F}\right)⇝\sum _{{k}\in {ℕ}_{0}}\left(\frac{{{A}}^{{k}}}{{k}!}\right)$
9 efval ${⊢}{A}\in ℂ\to {\mathrm{e}}^{{A}}=\sum _{{k}\in {ℕ}_{0}}\left(\frac{{{A}}^{{k}}}{{k}!}\right)$
10 8 9 breqtrrd ${⊢}{A}\in ℂ\to seq0\left(+,{F}\right)⇝{\mathrm{e}}^{{A}}$