Definition df-ef

Description: Define the exponential function. Its value at the complex number A is ( expA ) and is called the "exponential of A "; see efval . (Contributed by NM, 14-Mar-2005)

	Ref	Expression
Assertion	df-ef	|- exp = ( x e. CC |-> sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ce	|- exp
1		vx	|- x
2		cc	|- CC
3		vk	|- k
4		cn0	|- NN0
5	1	cv	|- x
6		cexp	|- ^
7	3	cv	|- k
8	5 7 6	co	|- ( x ^ k )
9		cdiv	|- /
10		cfa	|- !
11	7 10	cfv	|- ( ! ` k )
12	8 11 9	co	|- ( ( x ^ k ) / ( ! ` k ) )
13	4 12 3	csu	|- sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) )
14	1 2 13	cmpt	|- ( x e. CC |-> sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) ) )
15	0 14	wceq	|- exp = ( x e. CC |-> sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) ) )