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	⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
Assertion	efcvg	⊢ ( 𝐴 ∈ ℂ → seq 0 ( + , 𝐹 ) ⇝ ( exp ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		efcvg.1	⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
2		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
3		0zd	⊢ ( 𝐴 ∈ ℂ → 0 ∈ ℤ )
4	1	eftval	⊢ ( 𝑘 ∈ ℕ0 → ( 𝐹 ‘ 𝑘 ) = ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
5	4	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) = ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
6		eftcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
7	1	efcllem	⊢ ( 𝐴 ∈ ℂ → seq 0 ( + , 𝐹 ) ∈ dom ⇝ )
8	2 3 5 6 7	isumclim2	⊢ ( 𝐴 ∈ ℂ → seq 0 ( + , 𝐹 ) ⇝ Σ 𝑘 ∈ ℕ0 ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
9		efval	⊢ ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) = Σ 𝑘 ∈ ℕ0 ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
10	8 9	breqtrrd	⊢ ( 𝐴 ∈ ℂ → seq 0 ( + , 𝐹 ) ⇝ ( exp ‘ 𝐴 ) )