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 = ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( sin ‘ 𝑦 ) ≠ 0 } ↦ ( ( cos ‘ 𝑥 ) / ( sin ‘ 𝑥 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccot	⊢ cot
1		vx	⊢ 𝑥
2		vy	⊢ 𝑦
3		cc	⊢ ℂ
4		csin	⊢ sin
5	2	cv	⊢ 𝑦
6	5 4	cfv	⊢ ( sin ‘ 𝑦 )
7		cc0	⊢ 0
8	6 7	wne	⊢ ( sin ‘ 𝑦 ) ≠ 0
9	8 2 3	crab	⊢ { 𝑦 ∈ ℂ ∣ ( sin ‘ 𝑦 ) ≠ 0 }
10		ccos	⊢ cos
11	1	cv	⊢ 𝑥
12	11 10	cfv	⊢ ( cos ‘ 𝑥 )
13		cdiv	⊢ /
14	11 4	cfv	⊢ ( sin ‘ 𝑥 )
15	12 14 13	co	⊢ ( ( cos ‘ 𝑥 ) / ( sin ‘ 𝑥 ) )
16	1 9 15	cmpt	⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( sin ‘ 𝑦 ) ≠ 0 } ↦ ( ( cos ‘ 𝑥 ) / ( sin ‘ 𝑥 ) ) )
17	0 16	wceq	⊢ cot = ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( sin ‘ 𝑦 ) ≠ 0 } ↦ ( ( cos ‘ 𝑥 ) / ( sin ‘ 𝑥 ) ) )