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

Metamath Proof Explorer

Theorem efval

Description: Value of the exponential function. (Contributed by NM, 8-Jan-2006) (Revised by Mario Carneiro, 10-Nov-2013)

Ref Expression
Assertion efval ⊢ A ∈ ℂ → e A = ∑ k ∈ ℕ 0 A k k !

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ x = A → x k = A k
2 1 oveq1d ⊢ x = A → x k k ! = A k k !
3 2 sumeq2sdv ⊢ x = A → ∑ k ∈ ℕ 0 x k k ! = ∑ k ∈ ℕ 0 A k k !
4 df-ef ⊢ exp = x ∈ ℂ ⟼ ∑ k ∈ ℕ 0 x k k !
5 sumex ⊢ ∑ k ∈ ℕ 0 A k k ! ∈ V
6 3 4 5 fvmpt ⊢ A ∈ ℂ → e A = ∑ k ∈ ℕ 0 A k k !