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 e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )
Assertion	efcvg	|- ( A e. CC -> seq 0 ( + , F ) ~~> ( exp ` A ) )

Proof

Step	Hyp	Ref	Expression
1		efcvg.1	|- F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )
2		nn0uz	|- NN0 = ( ZZ>= ` 0 )
3		0zd	|- ( A e. CC -> 0 e. ZZ )
4	1	eftval	|- ( k e. NN0 -> ( F ` k ) = ( ( A ^ k ) / ( ! ` k ) ) )
5	4	adantl	|- ( ( A e. CC /\ k e. NN0 ) -> ( F ` k ) = ( ( A ^ k ) / ( ! ` k ) ) )
6		eftcl	|- ( ( A e. CC /\ k e. NN0 ) -> ( ( A ^ k ) / ( ! ` k ) ) e. CC )
7	1	efcllem	|- ( A e. CC -> seq 0 ( + , F ) e. dom ~~> )
8	2 3 5 6 7	isumclim2	|- ( A e. CC -> seq 0 ( + , F ) ~~> sum_ k e. NN0 ( ( A ^ k ) / ( ! ` k ) ) )
9		efval	|- ( A e. CC -> ( exp ` A ) = sum_ k e. NN0 ( ( A ^ k ) / ( ! ` k ) ) )
10	8 9	breqtrrd	|- ( A e. CC -> seq 0 ( + , F ) ~~> ( exp ` A ) )