Theorem efval2

Description: Value of the exponential function. (Contributed by Mario Carneiro, 29-Apr-2014)

	Ref	Expression
Hypothesis	efcvg.1	|- F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )
Assertion	efval2	|- ( A e. CC -> ( exp ` A ) = sum_ k e. NN0 ( F ` k ) )

Proof

Step	Hyp	Ref	Expression
1		efcvg.1	|- F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )
2		efval	|- ( A e. CC -> ( exp ` A ) = sum_ k e. NN0 ( ( A ^ k ) / ( ! ` k ) ) )
3	1	eftval	|- ( k e. NN0 -> ( F ` k ) = ( ( A ^ k ) / ( ! ` k ) ) )
4	3	sumeq2i	|- sum_ k e. NN0 ( F ` k ) = sum_ k e. NN0 ( ( A ^ k ) / ( ! ` k ) )
5	2 4	eqtr4di	|- ( A e. CC -> ( exp ` A ) = sum_ k e. NN0 ( F ` k ) )