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 ‘ 0 ) = 1

Proof

Step	Hyp	Ref	Expression
1		0cn	⊢ 0 ∈ ℂ
2		cos0	⊢ ( cos ‘ 0 ) = 1
3		ax-1ne0	⊢ 1 ≠ 0
4	2 3	eqnetri	⊢ ( cos ‘ 0 ) ≠ 0
5		secval	⊢ ( ( 0 ∈ ℂ ∧ ( cos ‘ 0 ) ≠ 0 ) → ( sec ‘ 0 ) = ( 1 / ( cos ‘ 0 ) ) )
6	1 4 5	mp2an	⊢ ( sec ‘ 0 ) = ( 1 / ( cos ‘ 0 ) )
7	2	oveq2i	⊢ ( 1 / ( cos ‘ 0 ) ) = ( 1 / 1 )
8		1div1e1	⊢ ( 1 / 1 ) = 1
9	6 7 8	3eqtri	⊢ ( sec ‘ 0 ) = 1