Theorem recsec

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

	Ref	Expression
Assertion	recsec	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to \cos A=\frac{1}{\sec \left(A\right)}$$

Proof

Step	Hyp	Ref	Expression
1		secval	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to \sec \left(A\right)=\frac{1}{\cos A}$$
2	1	oveq2d	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to \frac{1}{\sec \left(A\right)}=\frac{1}{\frac{1}{\cos A}}$$
3		coscl	$$⊢A\in ℂ\to \cos A\in ℂ$$
4		recrec	$$⊢\left(\cos A\in ℂ\wedge \cos A\ne 0\right)\to \frac{1}{\frac{1}{\cos A}}=\cos A$$
5	3 4	sylan	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to \frac{1}{\frac{1}{\cos A}}=\cos A$$
6	2 5	eqtr2d	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to \cos A=\frac{1}{\sec \left(A\right)}$$