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. CC -> ( exp ` A ) = sum_ k e. NN0 ( ( 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 -> sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) ) = sum_ k e. NN0 ( ( A ^ k ) / ( ! ` k ) ) )
4		df-ef	|- exp = ( x e. CC |-> sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) ) )
5		sumex	|- sum_ k e. NN0 ( ( A ^ k ) / ( ! ` k ) ) e. _V
6	3 4 5	fvmpt	|- ( A e. CC -> ( exp ` A ) = sum_ k e. NN0 ( ( A ^ k ) / ( ! ` k ) ) )