Metamath Proof Explorer


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