Definition df-cos

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

	Ref	Expression
Assertion	df-cos	$$⊢\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\cos$$
1		vx	$$setvarx$$
2		cc	$$classℂ$$
3		ce	$$class\exp$$
4		ci	$$class\mathrm{i}$$
5		cmul	$$class\times$$
6	1	cv	$$setvarx$$
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	$$class2$$
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\cos =\left(x\in ℂ⟼\frac{{\mathrm{e}}^{\mathrm{i}x}+{\mathrm{e}}^{\left(-\mathrm{i}\right)x}}{2}\right)$$