Metamath Proof Explorer


Theorem recotcl

Description: The closure of the cotangent function with a real argument. (Contributed by David A. Wheeler, 15-Mar-2014)

Ref Expression
Assertion recotcl ( ( 𝐴 ∈ ℝ ∧ ( sin ‘ 𝐴 ) ≠ 0 ) → ( cot ‘ 𝐴 ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 recn ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
2 cotval ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) ≠ 0 ) → ( cot ‘ 𝐴 ) = ( ( cos ‘ 𝐴 ) / ( sin ‘ 𝐴 ) ) )
3 1 2 sylan ( ( 𝐴 ∈ ℝ ∧ ( sin ‘ 𝐴 ) ≠ 0 ) → ( cot ‘ 𝐴 ) = ( ( cos ‘ 𝐴 ) / ( sin ‘ 𝐴 ) ) )
4 resincl ( 𝐴 ∈ ℝ → ( sin ‘ 𝐴 ) ∈ ℝ )
5 recoscl ( 𝐴 ∈ ℝ → ( cos ‘ 𝐴 ) ∈ ℝ )
6 redivcl ( ( ( cos ‘ 𝐴 ) ∈ ℝ ∧ ( sin ‘ 𝐴 ) ∈ ℝ ∧ ( sin ‘ 𝐴 ) ≠ 0 ) → ( ( cos ‘ 𝐴 ) / ( sin ‘ 𝐴 ) ) ∈ ℝ )
7 5 6 syl3an1 ( ( 𝐴 ∈ ℝ ∧ ( sin ‘ 𝐴 ) ∈ ℝ ∧ ( sin ‘ 𝐴 ) ≠ 0 ) → ( ( cos ‘ 𝐴 ) / ( sin ‘ 𝐴 ) ) ∈ ℝ )
8 4 7 syl3an2 ( ( 𝐴 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ ( sin ‘ 𝐴 ) ≠ 0 ) → ( ( cos ‘ 𝐴 ) / ( sin ‘ 𝐴 ) ) ∈ ℝ )
9 8 3anidm12 ( ( 𝐴 ∈ ℝ ∧ ( sin ‘ 𝐴 ) ≠ 0 ) → ( ( cos ‘ 𝐴 ) / ( sin ‘ 𝐴 ) ) ∈ ℝ )
10 3 9 eqeltrd ( ( 𝐴 ∈ ℝ ∧ ( sin ‘ 𝐴 ) ≠ 0 ) → ( cot ‘ 𝐴 ) ∈ ℝ )