Definition df-csc

Description: Define the cosecant function. We define it this way for cmpt , which requires the form ( x e. A |-> B ) . The csc function is defined in ISO 80000-2:2009(E) operation 2-13.7 and "NIST Digital Library of Mathematical Functions" section on "Trigonometric Functions" http://dlmf.nist.gov/4.14 . (Contributed by David A. Wheeler, 14-Mar-2014)

	Ref	Expression
Assertion	df-csc	|- csc = ( x e. { y e. CC | ( sin ` y ) =/= 0 } |-> ( 1 / ( sin ` x ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccsc	|- csc
1		vx	|- x
2		vy	|- y
3		cc	|- CC
4		csin	|- sin
5	2	cv	|- y
6	5 4	cfv	|- ( sin ` y )
7		cc0	|- 0
8	6 7	wne	|- ( sin ` y ) =/= 0
9	8 2 3	crab	|- { y e. CC | ( sin ` y ) =/= 0 }
10		c1	|- 1
11		cdiv	|- /
12	1	cv	|- x
13	12 4	cfv	|- ( sin ` x )
14	10 13 11	co	|- ( 1 / ( sin ` x ) )
15	1 9 14	cmpt	|- ( x e. { y e. CC | ( sin ` y ) =/= 0 } |-> ( 1 / ( sin ` x ) ) )
16	0 15	wceq	|- csc = ( x e. { y e. CC | ( sin ` y ) =/= 0 } |-> ( 1 / ( sin ` x ) ) )