Metamath Proof Explorer

Theorem recsec

Description: The reciprocal of secant is cosine. (Contributed by David A. Wheeler, 14-Mar-2014)

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

Proof

Step Hyp Ref Expression
1 secval 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( sec ` A ) = ( 1 / ( cos ` A ) ) )
2 1 oveq2d 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( 1 / ( sec ` A ) ) = ( 1 / ( 1 / ( cos ` A ) ) ) )
3 coscl 
 |-  ( A e. CC -> ( cos ` A ) e. CC )
4 recrec 
 |-  ( ( ( cos ` A ) e. CC /\ ( cos ` A ) =/= 0 ) -> ( 1 / ( 1 / ( cos ` A ) ) ) = ( cos ` A ) )
5 3 4 sylan 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( 1 / ( 1 / ( cos ` A ) ) ) = ( cos ` A ) )
6 2 5 eqtr2d 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( cos ` A ) = ( 1 / ( sec ` A ) ) )