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 =\left(x\in \left\{y\in ℂ|\sin y\ne 0\right\}⟼\frac{\cos x}{\sin x}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccot	$$class\cot$$
1		vx	$$setvarx$$
2		vy	$$setvary$$
3		cc	$$classℂ$$
4		csin	$$class\sin$$
5	2	cv	$$setvary$$
6	5 4	cfv	$$class\sin y$$
7		cc0	$$class0$$
8	6 7	wne	$$wff\sin y\ne 0$$
9	8 2 3	crab	$$class\left\{y\in ℂ|\sin y\ne 0\right\}$$
10		ccos	$$class\cos$$
11	1	cv	$$setvarx$$
12	11 10	cfv	$$class\cos x$$
13		cdiv	$$class÷$$
14	11 4	cfv	$$class\sin x$$
15	12 14 13	co	$$class\left(\frac{\cos x}{\sin x}\right)$$
16	1 9 15	cmpt	$$class\left(x\in \left\{y\in ℂ|\sin y\ne 0\right\}⟼\frac{\cos x}{\sin x}\right)$$
17	0 16	wceq	$$wff\cot =\left(x\in \left\{y\in ℂ|\sin y\ne 0\right\}⟼\frac{\cos x}{\sin x}\right)$$