Theorem reccsc

Description: The reciprocal of cosecant is sine. (Contributed by David A. Wheeler, 14-Mar-2014)

	Ref	Expression
Assertion	reccsc	$$⊢\left(A\in ℂ\wedge \sin A\ne 0\right)\to \sin A=\frac{1}{\csc \left(A\right)}$$

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	1	oveq2d	$$⊢\left(A\in ℂ\wedge \sin A\ne 0\right)\to \frac{1}{\csc \left(A\right)}=\frac{1}{\frac{1}{\sin A}}$$
3		sincl	$$⊢A\in ℂ\to \sin A\in ℂ$$
4		recrec	$$⊢\left(\sin A\in ℂ\wedge \sin A\ne 0\right)\to \frac{1}{\frac{1}{\sin A}}=\sin A$$
5	3 4	sylan	$$⊢\left(A\in ℂ\wedge \sin A\ne 0\right)\to \frac{1}{\frac{1}{\sin A}}=\sin A$$
6	2 5	eqtr2d	$$⊢\left(A\in ℂ\wedge \sin A\ne 0\right)\to \sin A=\frac{1}{\csc \left(A\right)}$$