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

Metamath Proof Explorer

Theorem efcvg

Description: The series that defines the exponential function converges to it. (Contributed by NM, 9-Jan-2006) (Revised by Mario Carneiro, 28-Apr-2014)

Ref Expression
Hypothesis efcvg.1 ⊢ F = n ∈ ℕ 0 ⟼ A n n !
Assertion efcvg ⊢ A ∈ ℂ → seq 0 + F ⇝ e A

Proof

Step Hyp Ref Expression
1 efcvg.1 ⊢ F = n ∈ ℕ 0 ⟼ A n n !
2 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
3 0zd ⊢ A ∈ ℂ → 0 ∈ ℤ
4 1 eftval ⊢ k ∈ ℕ 0 → F ⁡ k = A k k !
5 4 adantl ⊢ A ∈ ℂ ∧ k ∈ ℕ 0 → F ⁡ k = A k k !
6 eftcl ⊢ A ∈ ℂ ∧ k ∈ ℕ 0 → A k k ! ∈ ℂ
7 1 efcllem ⊢ A ∈ ℂ → seq 0 + F ∈ dom ⁡ ⇝
8 2 3 5 6 7 isumclim2 ⊢ A ∈ ℂ → seq 0 + F ⇝ ∑ k ∈ ℕ 0 A k k !
9 efval ⊢ A ∈ ℂ → e A = ∑ k ∈ ℕ 0 A k k !
10 8 9 breqtrrd ⊢ A ∈ ℂ → seq 0 + F ⇝ e A