Theorem csccl

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

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

Proof

Step	Hyp	Ref	Expression
1		cscval	|- ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( csc ` A ) = ( 1 / ( sin ` A ) ) )
2		sincl	|- ( A e. CC -> ( sin ` A ) e. CC )
3	2	adantr	|- ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( sin ` A ) e. CC )
4		simpr	|- ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( sin ` A ) =/= 0 )
5	3 4	reccld	|- ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( 1 / ( sin ` A ) ) e. CC )
6	1 5	eqeltrd	|- ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( csc ` A ) e. CC )