Theorem efval2

Description: Value of the exponential function. (Contributed by Mario Carneiro, 29-Apr-2014)

	Ref	Expression
Hypothesis	efcvg.1	$$⊢F=\left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)$$
Assertion	efval2	$$⊢A\in ℂ\to {\mathrm{e}}^A=\sum _{k\in {\mathbb{N}}_0}F\left(k\right)$$

Proof

Step	Hyp	Ref	Expression
1		efcvg.1	$$⊢F=\left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)$$
2		efval	$$⊢A\in ℂ\to {\mathrm{e}}^A=\sum _{k\in {\mathbb{N}}_0}\left(\frac{A^k}{k!}\right)$$
3	1	eftval	$$⊢k\in {\mathbb{N}}_0\to F\left(k\right)=\frac{A^k}{k!}$$
4	3	sumeq2i	$$⊢\sum _{k\in {\mathbb{N}}_0}F\left(k\right)=\sum _{k\in {\mathbb{N}}_0}\left(\frac{A^k}{k!}\right)$$
5	2 4	eqtr4di	$$⊢A\in ℂ\to {\mathrm{e}}^A=\sum _{k\in {\mathbb{N}}_0}F\left(k\right)$$