Metamath Proof Explorer


Theorem cotval

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

Ref Expression
Assertion cotval
|- ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( cot ` A ) = ( ( cos ` A ) / ( sin ` A ) ) )

Proof

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