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 = ( 𝑥 ∈ ( ◡ cos “ ( ℂ ∖ { 0 } ) ) ↦ ( ( sin ‘ 𝑥 ) / ( cos ‘ 𝑥 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctan	⊢ tan
1		vx	⊢ 𝑥
2		ccos	⊢ cos
3	2	ccnv	⊢ ◡ cos
4		cc	⊢ ℂ
5		cc0	⊢ 0
6	5	csn	⊢ { 0 }
7	4 6	cdif	⊢ ( ℂ ∖ { 0 } )
8	3 7	cima	⊢ ( ◡ cos “ ( ℂ ∖ { 0 } ) )
9		csin	⊢ sin
10	1	cv	⊢ 𝑥
11	10 9	cfv	⊢ ( sin ‘ 𝑥 )
12		cdiv	⊢ /
13	10 2	cfv	⊢ ( cos ‘ 𝑥 )
14	11 13 12	co	⊢ ( ( sin ‘ 𝑥 ) / ( cos ‘ 𝑥 ) )
15	1 8 14	cmpt	⊢ ( 𝑥 ∈ ( ◡ cos “ ( ℂ ∖ { 0 } ) ) ↦ ( ( sin ‘ 𝑥 ) / ( cos ‘ 𝑥 ) ) )
16	0 15	wceq	⊢ tan = ( 𝑥 ∈ ( ◡ cos “ ( ℂ ∖ { 0 } ) ) ↦ ( ( sin ‘ 𝑥 ) / ( cos ‘ 𝑥 ) ) )