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 = ( 𝑥 ∈ ℂ ↦ Σ 𝑘 ∈ ℕ0 ( ( 𝑥 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ce	⊢ exp
1		vx	⊢ 𝑥
2		cc	⊢ ℂ
3		vk	⊢ 𝑘
4		cn0	⊢ ℕ0
5	1	cv	⊢ 𝑥
6		cexp	⊢ ↑
7	3	cv	⊢ 𝑘
8	5 7 6	co	⊢ ( 𝑥 ↑ 𝑘 )
9		cdiv	⊢ /
10		cfa	⊢ !
11	7 10	cfv	⊢ ( ! ‘ 𝑘 )
12	8 11 9	co	⊢ ( ( 𝑥 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) )
13	4 12 3	csu	⊢ Σ 𝑘 ∈ ℕ0 ( ( 𝑥 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) )
14	1 2 13	cmpt	⊢ ( 𝑥 ∈ ℂ ↦ Σ 𝑘 ∈ ℕ0 ( ( 𝑥 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
15	0 14	wceq	⊢ exp = ( 𝑥 ∈ ℂ ↦ Σ 𝑘 ∈ ℕ0 ( ( 𝑥 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )