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 
|- ( ( A e. RR /\ ( sin ` A ) =/= 0 ) -> ( cot ` A ) e. RR )

Proof

Step Hyp Ref Expression
1 recn 
 |-  ( A e. RR -> A e. CC )
2 cotval 
 |-  ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( cot ` A ) = ( ( cos ` A ) / ( sin ` A ) ) )
3 1 2 sylan 
 |-  ( ( A e. RR /\ ( sin ` A ) =/= 0 ) -> ( cot ` A ) = ( ( cos ` A ) / ( sin ` A ) ) )
4 resincl 
 |-  ( A e. RR -> ( sin ` A ) e. RR )
5 recoscl 
 |-  ( A e. RR -> ( cos ` A ) e. RR )
6 redivcl 
 |-  ( ( ( cos ` A ) e. RR /\ ( sin ` A ) e. RR /\ ( sin ` A ) =/= 0 ) -> ( ( cos ` A ) / ( sin ` A ) ) e. RR )
7 5 6 syl3an1 
 |-  ( ( A e. RR /\ ( sin ` A ) e. RR /\ ( sin ` A ) =/= 0 ) -> ( ( cos ` A ) / ( sin ` A ) ) e. RR )
8 4 7 syl3an2 
 |-  ( ( A e. RR /\ A e. RR /\ ( sin ` A ) =/= 0 ) -> ( ( cos ` A ) / ( sin ` A ) ) e. RR )
9 8 3anidm12 
 |-  ( ( A e. RR /\ ( sin ` A ) =/= 0 ) -> ( ( cos ` A ) / ( sin ` A ) ) e. RR )
10 3 9 eqeltrd 
 |-  ( ( A e. RR /\ ( sin ` A ) =/= 0 ) -> ( cot ` A ) e. RR )