Metamath Proof Explorer


Definition df-cot

Description: Define the cotangent function. We define it this way for cmpt , which requires the form ( x e. A |-> B ) . The cot function is defined in ISO 80000-2:2009(E) operation 2-13.5 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-cot cot = x y | sin y 0 cos x sin x

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccot class cot
1 vx setvar x
2 vy setvar y
3 cc class
4 csin class sin
5 2 cv setvar y
6 5 4 cfv class sin y
7 cc0 class 0
8 6 7 wne wff sin y 0
9 8 2 3 crab class y | sin y 0
10 ccos class cos
11 1 cv setvar x
12 11 10 cfv class cos x
13 cdiv class ÷
14 11 4 cfv class sin x
15 12 14 13 co class cos x sin x
16 1 9 15 cmpt class x y | sin y 0 cos x sin x
17 0 16 wceq wff cot = x y | sin y 0 cos x sin x