Theorem rectan

Description: The reciprocal of tangent is cotangent. (Contributed by David A. Wheeler, 21-Mar-2014)

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

Proof

Step	Hyp	Ref	Expression
1		coscl	$$⊢A\in ℂ\to \cos A\in ℂ$$
2		sincl	$$⊢A\in ℂ\to \sin A\in ℂ$$
3		recdiv	$$⊢\left(\left(\sin A\in ℂ\wedge \sin A\ne 0\right)\wedge \left(\cos A\in ℂ\wedge \cos A\ne 0\right)\right)\to \frac{1}{\frac{\sin A}{\cos A}}=\frac{\cos A}{\sin A}$$
4	2 3	sylanl1	$$⊢\left(\left(A\in ℂ\wedge \sin A\ne 0\right)\wedge \left(\cos A\in ℂ\wedge \cos A\ne 0\right)\right)\to \frac{1}{\frac{\sin A}{\cos A}}=\frac{\cos A}{\sin A}$$
5	1 4	sylanr1	$$⊢\left(\left(A\in ℂ\wedge \sin A\ne 0\right)\wedge \left(A\in ℂ\wedge \cos A\ne 0\right)\right)\to \frac{1}{\frac{\sin A}{\cos A}}=\frac{\cos A}{\sin A}$$
6	5	3impdi	$$⊢\left(A\in ℂ\wedge \sin A\ne 0\wedge \cos A\ne 0\right)\to \frac{1}{\frac{\sin A}{\cos A}}=\frac{\cos A}{\sin A}$$
7		tanval	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to \tan A=\frac{\sin A}{\cos A}$$
8	7	3adant2	$$⊢\left(A\in ℂ\wedge \sin A\ne 0\wedge \cos A\ne 0\right)\to \tan A=\frac{\sin A}{\cos A}$$
9	8	oveq2d	$$⊢\left(A\in ℂ\wedge \sin A\ne 0\wedge \cos A\ne 0\right)\to \frac{1}{\tan A}=\frac{1}{\frac{\sin A}{\cos A}}$$
10		cotval	$$⊢\left(A\in ℂ\wedge \sin A\ne 0\right)\to \cot \left(A\right)=\frac{\cos A}{\sin A}$$
11	10	3adant3	$$⊢\left(A\in ℂ\wedge \sin A\ne 0\wedge \cos A\ne 0\right)\to \cot \left(A\right)=\frac{\cos A}{\sin A}$$
12	6 9 11	3eqtr4rd	$$⊢\left(A\in ℂ\wedge \sin A\ne 0\wedge \cos A\ne 0\right)\to \cot \left(A\right)=\frac{1}{\tan A}$$