Definition df-sin 7505

Description: Define the sine function.

Assertion

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

Distinct variable group:   x,y

Detailed syntax breakdown of Definition df-sin

Step	Hyp	Ref	Expression
1		csin 7500	. 2 class sin
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		cmin 5446	. . . . . . 7 class -
17	12, 15, 16	co 4021	. . . . . 6 class ((exp` (i x. x)) - (exp` (-ui x. x)))
18		c2 6107	. . . . . . 7 class 2
19	18, 8, 9	co 4021	. . . . . 6 class (2 x. i)
20		cdiv 5448	. . . . . 6 class /
21	17, 19, 20	co 4021	. . . . 5 class (((exp` (i x. x)) - (exp` (-ui x. x))) / (2 x. i))
22	7, 21	wceq 992	. . . 4 wff y = (((exp` (i x. x)) - (exp` (-ui x. x))) / (2 x. i))
23	5, 22	wa 221	. . 3 wff (x e. CC /\ y = (((exp` (i x. x)) - (exp` (-ui x. x))) / (2 x. i)))
24	23, 2, 6	copab 2740	. 2 class {<.x, y>. | (x e. CC /\ y = (((exp` (i x. x)) - (exp` (-ui x. x))) / (2 x. i)))}
25	1, 24	wceq 992	1 wff sin = {<.x, y>. | (x e. CC /\ y = (((exp` (i x. x)) - (exp` (-ui x. x))) / (2 x. i)))}

This definition is referenced by:  sinval 7637  sinf 7648

Copyright terms: Public domain