Definition df-cos

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

	Ref	Expression
Assertion	df-cos	|- cos = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) + ( exp ` ( -u _i x. x ) ) ) / 2 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccos	|- cos
1		vx	|- x
2		cc	|- CC
3		ce	|- exp
4		ci	|- _i
5		cmul	|- x.
6	1	cv	|- x
7	4 6 5	co	|- ( _i x. x )
8	7 3	cfv	|- ( exp ` ( _i x. x ) )
9		caddc	|- +
10	4	cneg	|- -u _i
11	10 6 5	co	|- ( -u _i x. x )
12	11 3	cfv	|- ( exp ` ( -u _i x. x ) )
13	8 12 9	co	|- ( ( exp ` ( _i x. x ) ) + ( exp ` ( -u _i x. x ) ) )
14		cdiv	|- /
15		c2	|- 2
16	13 15 14	co	|- ( ( ( exp ` ( _i x. x ) ) + ( exp ` ( -u _i x. x ) ) ) / 2 )
17	1 2 16	cmpt	|- ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) + ( exp ` ( -u _i x. x ) ) ) / 2 ) )
18	0 17	wceq	|- cos = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) + ( exp ` ( -u _i x. x ) ) ) / 2 ) )