Theorem sec0

Description: The value of the secant function at zero is one. (Contributed by David A. Wheeler, 16-Mar-2014)

	Ref	Expression
Assertion	sec0	$$⊢\sec \left(0\right)=1$$

Proof

Step	Hyp	Ref	Expression
1		0cn	$$⊢0\in ℂ$$
2		cos0	$$⊢\cos 0=1$$
3		ax-1ne0	$$⊢1\ne 0$$
4	2 3	eqnetri	$$⊢\cos 0\ne 0$$
5		secval	$$⊢\left(0\in ℂ\wedge \cos 0\ne 0\right)\to \sec \left(0\right)=\frac{1}{\cos 0}$$
6	1 4 5	mp2an	$$⊢\sec \left(0\right)=\frac{1}{\cos 0}$$
7	2	oveq2i	$$⊢\frac{1}{\cos 0}=\frac{1}{1}$$
8		1div1e1	$$⊢\frac{1}{1}=1$$
9	6 7 8	3eqtri	$$⊢\sec \left(0\right)=1$$