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 {\mathbb{N}}_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 {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)$$
2		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
3		0zd	$$⊢A\in ℂ\to 0\in \mathbb{Z}$$
4	1	eftval	$$⊢k\in {\mathbb{N}}_0\to F\left(k\right)=\frac{A^k}{k!}$$
5	4	adantl	$$⊢\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to F\left(k\right)=\frac{A^k}{k!}$$
6		eftcl	$$⊢\left(A\in ℂ\wedge k\in {\mathbb{N}}_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 {\mathbb{N}}_0}\left(\frac{A^k}{k!}\right)$$
9		efval	$$⊢A\in ℂ\to {\mathrm{e}}^A=\sum _{k\in {\mathbb{N}}_0}\left(\frac{A^k}{k!}\right)$$
10	8 9	breqtrrd	$$⊢A\in ℂ\to seq0\left(+,F\right)⇝{\mathrm{e}}^A$$