Theorem rectan

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

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

Proof

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