Description: Define the secant function. We define it this way for cmpt , which requires the form ( x e. A |-> B ) . The sec function is defined in ISO 80000-2:2009(E) operation 2-13.6 and "NIST Digital Library of Mathematical Functions" section on "Trigonometric Functions" http://dlmf.nist.gov/4.14 . (Contributed by David A. Wheeler, 14-Mar-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | df-sec | |- sec = ( x e. { y e. CC | ( cos ` y ) =/= 0 } |-> ( 1 / ( cos ` x ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | csec | |- sec |
|
1 | vx | |- x |
|
2 | vy | |- y |
|
3 | cc | |- CC |
|
4 | ccos | |- cos |
|
5 | 2 | cv | |- y |
6 | 5 4 | cfv | |- ( cos ` y ) |
7 | cc0 | |- 0 |
|
8 | 6 7 | wne | |- ( cos ` y ) =/= 0 |
9 | 8 2 3 | crab | |- { y e. CC | ( cos ` y ) =/= 0 } |
10 | c1 | |- 1 |
|
11 | cdiv | |- / |
|
12 | 1 | cv | |- x |
13 | 12 4 | cfv | |- ( cos ` x ) |
14 | 10 13 11 | co | |- ( 1 / ( cos ` x ) ) |
15 | 1 9 14 | cmpt | |- ( x e. { y e. CC | ( cos ` y ) =/= 0 } |-> ( 1 / ( cos ` x ) ) ) |
16 | 0 15 | wceq | |- sec = ( x e. { y e. CC | ( cos ` y ) =/= 0 } |-> ( 1 / ( cos ` x ) ) ) |