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 ‘ 𝐴 ) ∈ ℝ ) |