Definition df-sin 7492

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 7487	. 2 class sin
2		vx	. . . . . 6 set x
3	2	cv 988	. . . . 5 class x
4		cc 5377	. . . . 5 class CC
5	3, 4	wcel 991	. . . 4 wff x e. CC
6		vy	. . . . . 6 set y
7	6	cv 988	. . . . 5 class y
8		ci 5381	. . . . . . . . 9 class i
9		cmul 5384	. . . . . . . . 9 class x.
10	8, 3, 9	co 4016	. . . . . . . 8 class (i x. x)
11		ce 7485	. . . . . . . 8 class exp
12	10, 11	cfv 3260	. . . . . . 7 class (exp` (i x. x))
13	8	cneg 5438	. . . . . . . . 9 class -ui
14	13, 3, 9	co 4016	. . . . . . . 8 class (-ui x. x)
15	14, 11	cfv 3260	. . . . . . 7 class (exp` (-ui x. x))
16		cmin 5437	. . . . . . 7 class -
17	12, 15, 16	co 4016	. . . . . 6 class ((exp` (i x. x)) - (exp` (-ui x. x)))
18		c2 6098	. . . . . . 7 class 2
19	18, 8, 9	co 4016	. . . . . 6 class (2 x. i)
20		cdiv 5439	. . . . . 6 class /
21	17, 19, 20	co 4016	. . . . 5 class (((exp` (i x. x)) - (exp` (-ui x. x))) / (2 x. i))
22	7, 21	wceq 989	. . . 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 2735	. 2 class {<.x, y>. | (x e. CC /\ y = (((exp` (i x. x)) - (exp` (-ui x. x))) / (2 x. i)))}
25	1, 24	wceq 989	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 7624  sinf 7635

Copyright terms: Public domain