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	$$⊢\left(A\in ℂ\wedge \sin A\ne 0\right)\to \csc \left(A\right)\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		cscval	$$⊢\left(A\in ℂ\wedge \sin A\ne 0\right)\to \csc \left(A\right)=\frac{1}{\sin A}$$
2		sincl	$$⊢A\in ℂ\to \sin A\in ℂ$$
3	2	adantr	$$⊢\left(A\in ℂ\wedge \sin A\ne 0\right)\to \sin A\in ℂ$$
4		simpr	$$⊢\left(A\in ℂ\wedge \sin A\ne 0\right)\to \sin A\ne 0$$
5	3 4	reccld	$$⊢\left(A\in ℂ\wedge \sin A\ne 0\right)\to \frac{1}{\sin A}\in ℂ$$
6	1 5	eqeltrd	$$⊢\left(A\in ℂ\wedge \sin A\ne 0\right)\to \csc \left(A\right)\in ℂ$$