Mathbox for David A. Wheeler < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-cot Structured version   Unicode version

Definition df-cot 28489
 Description: Define the cotangent function. We define it this way for cmpt 4266, which requires the form . 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.)
Assertion
Ref Expression
df-cot
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-cot
StepHypRef Expression
1 ccot 28486 . 2
2 vx . . 3
3 vy . . . . . . 7
43cv 1651 . . . . . 6
5 csin 12666 . . . . . 6
64, 5cfv 5454 . . . . 5
7 cc0 8990 . . . . 5
86, 7wne 2599 . . . 4
9 cc 8988 . . . 4
108, 3, 9crab 2709 . . 3
112cv 1651 . . . . 5
12 ccos 12667 . . . . 5
1311, 12cfv 5454 . . . 4
1411, 5cfv 5454 . . . 4
15 cdiv 9677 . . . 4
1613, 14, 15co 6081 . . 3
172, 10, 16cmpt 4266 . 2
181, 17wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  cotval  28492
 Copyright terms: Public domain W3C validator