Theorem efval

Description: Value of the exponential function. (Contributed by NM, 8-Jan-2006) (Revised by Mario Carneiro, 10-Nov-2013)

	Ref	Expression
Assertion	efval	$$⊢A\in ℂ\to {\mathrm{e}}^A=\sum _{k\in {\mathbb{N}}_0}\left(\frac{A^k}{k!}\right)$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$$⊢x=A\to x^k=A^k$$
2	1	oveq1d	$$⊢x=A\to \frac{x^k}{k!}=\frac{A^k}{k!}$$
3	2	sumeq2sdv	$$⊢x=A\to \sum _{k\in {\mathbb{N}}_0}\left(\frac{x^k}{k!}\right)=\sum _{k\in {\mathbb{N}}_0}\left(\frac{A^k}{k!}\right)$$
4		df-ef	$$⊢\exp =\left(x\in ℂ⟼\sum _{k\in {\mathbb{N}}_0}\left(\frac{x^k}{k!}\right)\right)$$
5		sumex	$$⊢\sum _{k\in {\mathbb{N}}_0}\left(\frac{A^k}{k!}\right)\in \mathrm{V}$$
6	3 4 5	fvmpt	$$⊢A\in ℂ\to {\mathrm{e}}^A=\sum _{k\in {\mathbb{N}}_0}\left(\frac{A^k}{k!}\right)$$