Theorem eff

Description: Domain and codomain of the exponential function. (Contributed by Paul Chapman, 22-Oct-2007) (Proof shortened by Mario Carneiro, 28-Apr-2014)

	Ref	Expression
Assertion	eff	$$⊢\exp :ℂ⟶ℂ$$

Proof

Step	Hyp	Ref	Expression
1		df-ef	$$⊢\exp =\left(x\in ℂ⟼\sum _{k\in {\mathbb{N}}_0}\left(\frac{x^k}{k!}\right)\right)$$
2		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
3		0zd	$$⊢x\in ℂ\to 0\in \mathbb{Z}$$
4		eqid	$$⊢\left(n\in {\mathbb{N}}_0⟼\frac{x^n}{n!}\right)=\left(n\in {\mathbb{N}}_0⟼\frac{x^n}{n!}\right)$$
5	4	eftval	$$⊢k\in {\mathbb{N}}_0\to \left(n\in {\mathbb{N}}_0⟼\frac{x^n}{n!}\right)\left(k\right)=\frac{x^k}{k!}$$
6	5	adantl	$$⊢\left(x\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to \left(n\in {\mathbb{N}}_0⟼\frac{x^n}{n!}\right)\left(k\right)=\frac{x^k}{k!}$$
7		eftcl	$$⊢\left(x\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to \frac{x^k}{k!}\in ℂ$$
8	4	efcllem	$$⊢x\in ℂ\to seq0\left(+,\left(n\in {\mathbb{N}}_0⟼\frac{x^n}{n!}\right)\right)\in \mathrm{dom}⇝$$
9	2 3 6 7 8	isumcl	$$⊢x\in ℂ\to \sum _{k\in {\mathbb{N}}_0}\left(\frac{x^k}{k!}\right)\in ℂ$$
10	1 9	fmpti	$$⊢\exp :ℂ⟶ℂ$$