Metamath Proof Explorer


Definition df-sec

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 ) ) )

Detailed syntax breakdown

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 ) ) )