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 = x ∈ ℂ ⟼ ∑ k ∈ ℕ 0 x k k !
2 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
3 0zd ⊢ x ∈ ℂ → 0 ∈ ℤ
4 eqid ⊢ n ∈ ℕ 0 ⟼ x n n ! = n ∈ ℕ 0 ⟼ x n n !
5 4 eftval ⊢ k ∈ ℕ 0 → n ∈ ℕ 0 ⟼ x n n ! ⁡ k = x k k !
6 5 adantl ⊢ x ∈ ℂ ∧ k ∈ ℕ 0 → n ∈ ℕ 0 ⟼ x n n ! ⁡ k = x k k !
7 eftcl ⊢ x ∈ ℂ ∧ k ∈ ℕ 0 → x k k ! ∈ ℂ
8 4 efcllem ⊢ x ∈ ℂ → seq 0 + n ∈ ℕ 0 ⟼ x n n ! ∈ dom ⁡ ⇝
9 2 3 6 7 8 isumcl ⊢ x ∈ ℂ → ∑ k ∈ ℕ 0 x k k ! ∈ ℂ
10 1 9 fmpti ⊢ exp : ℂ ⟶ ℂ