Metamath Proof Explorer


Theorem secval

Description: Value of the secant function. (Contributed by David A. Wheeler, 14-Mar-2014)

Ref Expression
Assertion secval
|- ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( sec ` A ) = ( 1 / ( cos ` A ) ) )

Proof

Step Hyp Ref Expression
1 fveq2
 |-  ( y = A -> ( cos ` y ) = ( cos ` A ) )
2 1 neeq1d
 |-  ( y = A -> ( ( cos ` y ) =/= 0 <-> ( cos ` A ) =/= 0 ) )
3 2 elrab
 |-  ( A e. { y e. CC | ( cos ` y ) =/= 0 } <-> ( A e. CC /\ ( cos ` A ) =/= 0 ) )
4 fveq2
 |-  ( x = A -> ( cos ` x ) = ( cos ` A ) )
5 4 oveq2d
 |-  ( x = A -> ( 1 / ( cos ` x ) ) = ( 1 / ( cos ` A ) ) )
6 df-sec
 |-  sec = ( x e. { y e. CC | ( cos ` y ) =/= 0 } |-> ( 1 / ( cos ` x ) ) )
7 ovex
 |-  ( 1 / ( cos ` A ) ) e. _V
8 5 6 7 fvmpt
 |-  ( A e. { y e. CC | ( cos ` y ) =/= 0 } -> ( sec ` A ) = ( 1 / ( cos ` A ) ) )
9 3 8 sylbir
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( sec ` A ) = ( 1 / ( cos ` A ) ) )