Definition df-sin

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csin	|- sin
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		cmin	|- -
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	15 4 5	co	|- ( 2 x. _i )
17	13 16 14	co	|- ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) )
18	1 2 17	cmpt	|- ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) ) )
19	0 18	wceq	|- sin = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) ) )