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 = x ∈ ℂ ⟼ e i ⁢ x + e − i ⁢ x 2

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccos class cos
1 vx setvar x
2 cc class ℂ
3 ce class exp
4 ci class i
5 cmul class ×
6 1 cv setvar x
7 4 6 5 co class i ⁢ x
8 7 3 cfv class e i ⁢ x
9 caddc class +
10 4 cneg class − i
11 10 6 5 co class − i ⁢ x
12 11 3 cfv class e − i ⁢ x
13 8 12 9 co class e i ⁢ x + e − i ⁢ x
14 cdiv class ÷
15 c2 class 2
16 13 15 14 co class e i ⁢ x + e − i ⁢ x 2
17 1 2 16 cmpt class x ∈ ℂ ⟼ e i ⁢ x + e − i ⁢ x 2
18 0 17 wceq wff cos = x ∈ ℂ ⟼ e i ⁢ x + e − i ⁢ x 2