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 =\left(x\in ℂ⟼\sum _{k\in {\mathbb{N}}_0}\left(\frac{x^k}{k!}\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ce	$$class\exp$$
1		vx	$$setvarx$$
2		cc	$$classℂ$$
3		vk	$$setvark$$
4		cn0	$$class{\mathbb{N}}_0$$
5	1	cv	$$setvarx$$
6		cexp	$$class^$$
7	3	cv	$$setvark$$
8	5 7 6	co	$$class{x}^k$$
9		cdiv	$$class÷$$
10		cfa	$$class!$$
11	7 10	cfv	$$classk!$$
12	8 11 9	co	$$class\left(\frac{x^k}{k!}\right)$$
13	4 12 3	csu	$$class\sum _{k\in {\mathbb{N}}_0}\left(\frac{x^k}{k!}\right)$$
14	1 2 13	cmpt	$$class\left(x\in ℂ⟼\sum _{k\in {\mathbb{N}}_0}\left(\frac{x^k}{k!}\right)\right)$$
15	0 14	wceq	$$wff\exp =\left(x\in ℂ⟼\sum _{k\in {\mathbb{N}}_0}\left(\frac{x^k}{k!}\right)\right)$$