Theorem seccl

Description: The closure of the secant function with a complex argument. (Contributed by David A. Wheeler, 14-Mar-2014)

	Ref	Expression
Assertion	seccl	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to \sec \left(A\right)\in ℂ$$

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		coscl	$$⊢A\in ℂ\to \cos A\in ℂ$$
3	2	adantr	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to \cos A\in ℂ$$
4		simpr	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to \cos A\ne 0$$
5	3 4	reccld	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to \frac{1}{\cos A}\in ℂ$$
6	1 5	eqeltrd	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to \sec \left(A\right)\in ℂ$$