Theorem secval

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

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

Proof

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