Description: The value of the secant function at zero is one. (Contributed by David A. Wheeler, 16-Mar-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | sec0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0cn | ||
2 | cos0 | ||
3 | ax-1ne0 | ||
4 | 2 3 | eqnetri | |
5 | secval | ||
6 | 1 4 5 | mp2an | |
7 | 2 | oveq2i | |
8 | 1div1e1 | ||
9 | 6 7 8 | 3eqtri |