Definition df-tan

Description: Define the tangent function. We define it this way for cmpt , which requires the form ( x e. A |-> B ) . (Contributed by Mario Carneiro, 14-Mar-2014)

	Ref	Expression
Assertion	df-tan	|- tan = ( x e. ( `' cos " ( CC \ { 0 } ) ) |-> ( ( sin ` x ) / ( cos ` x ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctan	|- tan
1		vx	|- x
2		ccos	|- cos
3	2	ccnv	|- `' cos
4		cc	|- CC
5		cc0	|- 0
6	5	csn	|- { 0 }
7	4 6	cdif	|- ( CC \ { 0 } )
8	3 7	cima	|- ( `' cos " ( CC \ { 0 } ) )
9		csin	|- sin
10	1	cv	|- x
11	10 9	cfv	|- ( sin ` x )
12		cdiv	|- /
13	10 2	cfv	|- ( cos ` x )
14	11 13 12	co	|- ( ( sin ` x ) / ( cos ` x ) )
15	1 8 14	cmpt	|- ( x e. ( `' cos " ( CC \ { 0 } ) ) |-> ( ( sin ` x ) / ( cos ` x ) ) )
16	0 15	wceq	|- tan = ( x e. ( `' cos " ( CC \ { 0 } ) ) |-> ( ( sin ` x ) / ( cos ` x ) ) )