Metamath Proof Explorer

Theorem cotcl

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

Ref Expression
Assertion cotcl 
|- ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( cot ` A ) e. CC )

Proof

Step Hyp Ref Expression
1 cotval 
 |-  ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( cot ` A ) = ( ( cos ` A ) / ( sin ` A ) ) )
2 coscl 
 |-  ( A e. CC -> ( cos ` A ) e. CC )
3 2 adantr 
 |-  ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( cos ` A ) e. CC )
4 sincl 
 |-  ( A e. CC -> ( sin ` A ) e. CC )
5 4 adantr 
 |-  ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( sin ` A ) e. CC )
6 simpr 
 |-  ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( sin ` A ) =/= 0 )
7 3 5 6 divcld 
 |-  ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( ( cos ` A ) / ( sin ` A ) ) e. CC )
8 1 7 eqeltrd 
 |-  ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( cot ` A ) e. CC )