This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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