Definition df-cos

Description: Define the cosine function. (Contributed by NM, 14-Mar-2005)

	Ref	Expression
Assertion	df-cos	⊢ cos = ( 𝑥 ∈ ℂ ↦ ( ( ( exp ‘ ( i · 𝑥 ) ) + ( exp ‘ ( - i · 𝑥 ) ) ) / 2 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccos	⊢ cos
1		vx	⊢ 𝑥
2		cc	⊢ ℂ
3		ce	⊢ exp
4		ci	⊢ i
5		cmul	⊢ ·
6	1	cv	⊢ 𝑥
7	4 6 5	co	⊢ ( i · 𝑥 )
8	7 3	cfv	⊢ ( exp ‘ ( i · 𝑥 ) )
9		caddc	⊢ +
10	4	cneg	⊢ - i
11	10 6 5	co	⊢ ( - i · 𝑥 )
12	11 3	cfv	⊢ ( exp ‘ ( - i · 𝑥 ) )
13	8 12 9	co	⊢ ( ( exp ‘ ( i · 𝑥 ) ) + ( exp ‘ ( - i · 𝑥 ) ) )
14		cdiv	⊢ /
15		c2	⊢ 2
16	13 15 14	co	⊢ ( ( ( exp ‘ ( i · 𝑥 ) ) + ( exp ‘ ( - i · 𝑥 ) ) ) / 2 )
17	1 2 16	cmpt	⊢ ( 𝑥 ∈ ℂ ↦ ( ( ( exp ‘ ( i · 𝑥 ) ) + ( exp ‘ ( - i · 𝑥 ) ) ) / 2 ) )
18	0 17	wceq	⊢ cos = ( 𝑥 ∈ ℂ ↦ ( ( ( exp ‘ ( i · 𝑥 ) ) + ( exp ‘ ( - i · 𝑥 ) ) ) / 2 ) )