Theorem cotval

Description: Value of the cotangent function. (Contributed by David A. Wheeler, 14-Mar-2014)

	Ref	Expression
Assertion	cotval	$$⊢\left(A\in ℂ\wedge \sin A\ne 0\right)\to \cot \left(A\right)=\frac{\cos A}{\sin A}$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢y=A\to \sin y=\sin A$$
2	1	neeq1d	$$⊢y=A\to \left(\sin y\ne 0\leftrightarrow \sin A\ne 0\right)$$
3	2	elrab	$$⊢A\in \left\{y\in ℂ|\sin y\ne 0\right\}\leftrightarrow \left(A\in ℂ\wedge \sin A\ne 0\right)$$
4		fveq2	$$⊢x=A\to \cos x=\cos A$$
5		fveq2	$$⊢x=A\to \sin x=\sin A$$
6	4 5	oveq12d	$$⊢x=A\to \frac{\cos x}{\sin x}=\frac{\cos A}{\sin A}$$
7		df-cot	$$⊢\cot =\left(x\in \left\{y\in ℂ|\sin y\ne 0\right\}⟼\frac{\cos x}{\sin x}\right)$$
8		ovex	$$⊢\frac{\cos A}{\sin A}\in \mathrm{V}$$
9	6 7 8	fvmpt	$$⊢A\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \cot \left(A\right)=\frac{\cos A}{\sin A}$$
10	3 9	sylbir	$$⊢\left(A\in ℂ\wedge \sin A\ne 0\right)\to \cot \left(A\right)=\frac{\cos A}{\sin A}$$