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 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0cn | |- 0 e. CC |
|
| 2 | cos0 | |- ( cos ` 0 ) = 1 |
|
| 3 | ax-1ne0 | |- 1 =/= 0 |
|
| 4 | 2 3 | eqnetri | |- ( cos ` 0 ) =/= 0 |
| 5 | secval | |- ( ( 0 e. CC /\ ( 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 |