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 = ( 𝑥 ∈ ℂ ↦ Σ 𝑘 ∈ ℕ0 ( ( 𝑥 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
2		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
3		0zd	⊢ ( 𝑥 ∈ ℂ → 0 ∈ ℤ )
4		eqid	⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑥 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑥 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
5	4	eftval	⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑥 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) = ( ( 𝑥 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
6	5	adantl	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑥 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) = ( ( 𝑥 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
7		eftcl	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑥 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
8	4	efcllem	⊢ ( 𝑥 ∈ ℂ → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑥 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ∈ dom ⇝ )
9	2 3 6 7 8	isumcl	⊢ ( 𝑥 ∈ ℂ → Σ 𝑘 ∈ ℕ0 ( ( 𝑥 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
10	1 9	fmpti	⊢ exp : ℂ ⟶ ℂ