Metamath Proof Explorer

Theorem reccsc

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

Ref Expression
Assertion reccsc 
|- ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( sin ` A ) = ( 1 / ( csc ` A ) ) )

Proof

Step Hyp Ref Expression
1 cscval 
 |-  ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( csc ` A ) = ( 1 / ( sin ` A ) ) )
2 1 oveq2d 
 |-  ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( 1 / ( csc ` A ) ) = ( 1 / ( 1 / ( sin ` A ) ) ) )
3 sincl 
 |-  ( A e. CC -> ( sin ` A ) e. CC )
4 recrec 
 |-  ( ( ( sin ` A ) e. CC /\ ( sin ` A ) =/= 0 ) -> ( 1 / ( 1 / ( sin ` A ) ) ) = ( sin ` A ) )
5 3 4 sylan 
 |-  ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( 1 / ( 1 / ( sin ` A ) ) ) = ( sin ` A ) )
6 2 5 eqtr2d 
 |-  ( ( A e. CC /\ ( sin ` A ) =/= 0 ) -> ( sin ` A ) = ( 1 / ( csc ` A ) ) )