Theorem reccot

Description: The reciprocal of cotangent is tangent. (Contributed by David A. Wheeler, 21-Mar-2014)

	Ref	Expression
Assertion	reccot	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( tan ‘ 𝐴 ) = ( 1 / ( cot ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sincl	⊢ ( 𝐴 ∈ ℂ → ( sin ‘ 𝐴 ) ∈ ℂ )
2		coscl	⊢ ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) ∈ ℂ )
3		recdiv	⊢ ( ( ( ( cos ‘ 𝐴 ) ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) ∧ ( ( sin ‘ 𝐴 ) ∈ ℂ ∧ ( sin ‘ 𝐴 ) ≠ 0 ) ) → ( 1 / ( ( cos ‘ 𝐴 ) / ( sin ‘ 𝐴 ) ) ) = ( ( sin ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) )
4	2 3	sylanl1	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) ∧ ( ( sin ‘ 𝐴 ) ∈ ℂ ∧ ( sin ‘ 𝐴 ) ≠ 0 ) ) → ( 1 / ( ( cos ‘ 𝐴 ) / ( sin ‘ 𝐴 ) ) ) = ( ( sin ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) )
5	1 4	sylanr1	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) ≠ 0 ) ) → ( 1 / ( ( cos ‘ 𝐴 ) / ( sin ‘ 𝐴 ) ) ) = ( ( sin ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) )
6	5	3impdi	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ∧ ( sin ‘ 𝐴 ) ≠ 0 ) → ( 1 / ( ( cos ‘ 𝐴 ) / ( sin ‘ 𝐴 ) ) ) = ( ( sin ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) )
7	6	3com23	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( 1 / ( ( cos ‘ 𝐴 ) / ( sin ‘ 𝐴 ) ) ) = ( ( sin ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) )
8		cotval	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) ≠ 0 ) → ( cot ‘ 𝐴 ) = ( ( cos ‘ 𝐴 ) / ( sin ‘ 𝐴 ) ) )
9	8	3adant3	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( cot ‘ 𝐴 ) = ( ( cos ‘ 𝐴 ) / ( sin ‘ 𝐴 ) ) )
10	9	oveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( 1 / ( cot ‘ 𝐴 ) ) = ( 1 / ( ( cos ‘ 𝐴 ) / ( sin ‘ 𝐴 ) ) ) )
11		tanval	⊢ ( ( 𝐴 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( tan ‘ 𝐴 ) = ( ( sin ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) )
12	11	3adant2	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( tan ‘ 𝐴 ) = ( ( sin ‘ 𝐴 ) / ( cos ‘ 𝐴 ) ) )
13	7 10 12	3eqtr4rd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) ≠ 0 ∧ ( cos ‘ 𝐴 ) ≠ 0 ) → ( tan ‘ 𝐴 ) = ( 1 / ( cot ‘ 𝐴 ) ) )