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 = x ∈ cos -1 ℂ ∖ 0 ⟼ sin ⁡ x cos ⁡ x

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctan class tan
1 vx setvar x
2 ccos class cos
3 2 ccnv class cos -1
4 cc class ℂ
5 cc0 class 0
6 5 csn class 0
7 4 6 cdif class ℂ ∖ 0
8 3 7 cima class cos -1 ℂ ∖ 0
9 csin class sin
10 1 cv setvar x
11 10 9 cfv class sin ⁡ x
12 cdiv class ÷
13 10 2 cfv class cos ⁡ x
14 11 13 12 co class sin ⁡ x cos ⁡ x
15 1 8 14 cmpt class x ∈ cos -1 ℂ ∖ 0 ⟼ sin ⁡ x cos ⁡ x
16 0 15 wceq wff tan = x ∈ cos -1 ℂ ∖ 0 ⟼ sin ⁡ x cos ⁡ x