This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 : ℂ ⟶ ℂ