Theorem reccot

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

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

Proof

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