Metamath Proof Explorer


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 ) )