Definition df-cos 7506

Description: Define the cosine function.

Assertion

Ref	Expression
df-cos	|- cos = {<.x, y>. | (x e. CC /\ y = (((exp` (i x. x)) + (exp` (-ui x. x))) / 2))}

Distinct variable group:   x,y

Detailed syntax breakdown of Definition df-cos

Step	Hyp	Ref	Expression
1		ccos 7501	. 2 class cos
2		vx	. . . . . 6 set x
3	2	cv 991	. . . . 5 class x
4		cc 5386	. . . . 5 class CC
5	3, 4	wcel 994	. . . 4 wff x e. CC
6		vy	. . . . . 6 set y
7	6	cv 991	. . . . 5 class y
8		ci 5390	. . . . . . . . 9 class i
9		cmul 5393	. . . . . . . . 9 class x.
10	8, 3, 9	co 4021	. . . . . . . 8 class (i x. x)
11		ce 7498	. . . . . . . 8 class exp
12	10, 11	cfv 3263	. . . . . . 7 class (exp` (i x. x))
13	8	cneg 5447	. . . . . . . . 9 class -ui
14	13, 3, 9	co 4021	. . . . . . . 8 class (-ui x. x)
15	14, 11	cfv 3263	. . . . . . 7 class (exp` (-ui x. x))
16		caddc 5391	. . . . . . 7 class +
17	12, 15, 16	co 4021	. . . . . 6 class ((exp` (i x. x)) + (exp` (-ui x. x)))
18		c2 6107	. . . . . 6 class 2
19		cdiv 5448	. . . . . 6 class /
20	17, 18, 19	co 4021	. . . . 5 class (((exp` (i x. x)) + (exp` (-ui x. x))) / 2)
21	7, 20	wceq 992	. . . 4 wff y = (((exp` (i x. x)) + (exp` (-ui x. x))) / 2)
22	5, 21	wa 221	. . 3 wff (x e. CC /\ y = (((exp` (i x. x)) + (exp` (-ui x. x))) / 2))
23	22, 2, 6	copab 2740	. 2 class {<.x, y>. | (x e. CC /\ y = (((exp` (i x. x)) + (exp` (-ui x. x))) / 2))}
24	1, 23	wceq 992	1 wff cos = {<.x, y>. | (x e. CC /\ y = (((exp` (i x. x)) + (exp` (-ui x. x))) / 2))}

This definition is referenced by:  cosval 7638  cosf 7649

Copyright terms: Public domain