This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑥 ) ) )