# Metamath Proof Explorer

## Definition df-cos

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

Ref Expression
Assertion df-cos ${⊢}\mathrm{cos}=\left({x}\in ℂ⟼\frac{{\mathrm{e}}^{\mathrm{i}{x}}+{\mathrm{e}}^{\left(-\mathrm{i}\right){x}}}{2}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 ccos ${class}\mathrm{cos}$
1 vx ${setvar}{x}$
2 cc ${class}ℂ$
3 ce ${class}\mathrm{exp}$
4 ci ${class}\mathrm{i}$
5 cmul ${class}×$
6 1 cv ${setvar}{x}$
7 4 6 5 co ${class}\mathrm{i}{x}$
8 7 3 cfv ${class}{\mathrm{e}}^{\mathrm{i}{x}}$
9 caddc ${class}+$
10 4 cneg ${class}\left(-\mathrm{i}\right)$
11 10 6 5 co ${class}\left(-\mathrm{i}\right){x}$
12 11 3 cfv ${class}{\mathrm{e}}^{\left(-\mathrm{i}\right){x}}$
13 8 12 9 co ${class}\left({\mathrm{e}}^{\mathrm{i}{x}}+{\mathrm{e}}^{\left(-\mathrm{i}\right){x}}\right)$
14 cdiv ${class}÷$
15 c2 ${class}2$
16 13 15 14 co ${class}\left(\frac{{\mathrm{e}}^{\mathrm{i}{x}}+{\mathrm{e}}^{\left(-\mathrm{i}\right){x}}}{2}\right)$
17 1 2 16 cmpt ${class}\left({x}\in ℂ⟼\frac{{\mathrm{e}}^{\mathrm{i}{x}}+{\mathrm{e}}^{\left(-\mathrm{i}\right){x}}}{2}\right)$
18 0 17 wceq ${wff}\mathrm{cos}=\left({x}\in ℂ⟼\frac{{\mathrm{e}}^{\mathrm{i}{x}}+{\mathrm{e}}^{\left(-\mathrm{i}\right){x}}}{2}\right)$