Metamath Proof Explorer

Theorem sinneg

Description: The sine of a negative is the negative of the sine. (Contributed by NM, 30-Apr-2005)

Ref Expression
Assertion sinneg 
|- ( A e. CC -> ( sin ` -u A ) = -u ( sin ` A ) )

Proof

Step Hyp Ref Expression
1 negcl 
 |-  ( A e. CC -> -u A e. CC )
2 sinval 
 |-  ( -u A e. CC -> ( sin ` -u A ) = ( ( ( exp ` ( _i x. -u A ) ) - ( exp ` ( -u _i x. -u A ) ) ) / ( 2 x. _i ) ) )
3 1 2 syl 
 |-  ( A e. CC -> ( sin ` -u A ) = ( ( ( exp ` ( _i x. -u A ) ) - ( exp ` ( -u _i x. -u A ) ) ) / ( 2 x. _i ) ) )
4 sinval 
 |-  ( A e. CC -> ( sin ` A ) = ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( 2 x. _i ) ) )
5 4 negeqd 
 |-  ( A e. CC -> -u ( sin ` A ) = -u ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( 2 x. _i ) ) )
6 ax-icn 
 |-  _i e. CC
7 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
8 6 7 mpan 
 |-  ( A e. CC -> ( _i x. A ) e. CC )
9 efcl 
 |-  ( ( _i x. A ) e. CC -> ( exp ` ( _i x. A ) ) e. CC )
10 8 9 syl 
 |-  ( A e. CC -> ( exp ` ( _i x. A ) ) e. CC )
11 negicn 
 |-  -u _i e. CC
12 mulcl 
 |-  ( ( -u _i e. CC /\ A e. CC ) -> ( -u _i x. A ) e. CC )
13 11 12 mpan 
 |-  ( A e. CC -> ( -u _i x. A ) e. CC )
14 efcl 
 |-  ( ( -u _i x. A ) e. CC -> ( exp ` ( -u _i x. A ) ) e. CC )
15 13 14 syl 
 |-  ( A e. CC -> ( exp ` ( -u _i x. A ) ) e. CC )
16 10 15 subcld 
 |-  ( A e. CC -> ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) e. CC )
17 2mulicn 
 |-  ( 2 x. _i ) e. CC
18 2muline0 
 |-  ( 2 x. _i ) =/= 0
19 divneg 
 |-  ( ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) e. CC /\ ( 2 x. _i ) e. CC /\ ( 2 x. _i ) =/= 0 ) -> -u ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( 2 x. _i ) ) = ( -u ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( 2 x. _i ) ) )
20 17 18 19 mp3an23 
 |-  ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) e. CC -> -u ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( 2 x. _i ) ) = ( -u ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( 2 x. _i ) ) )
21 16 20 syl 
 |-  ( A e. CC -> -u ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( 2 x. _i ) ) = ( -u ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( 2 x. _i ) ) )
22 5 21 eqtrd 
 |-  ( A e. CC -> -u ( sin ` A ) = ( -u ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( 2 x. _i ) ) )
23 mulneg12 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( -u _i x. A ) = ( _i x. -u A ) )
24 6 23 mpan 
 |-  ( A e. CC -> ( -u _i x. A ) = ( _i x. -u A ) )
25 24 eqcomd 
 |-  ( A e. CC -> ( _i x. -u A ) = ( -u _i x. A ) )
26 25 fveq2d 
 |-  ( A e. CC -> ( exp ` ( _i x. -u A ) ) = ( exp ` ( -u _i x. A ) ) )
27 mul2neg 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( -u _i x. -u A ) = ( _i x. A ) )
28 6 27 mpan 
 |-  ( A e. CC -> ( -u _i x. -u A ) = ( _i x. A ) )
29 28 fveq2d 
 |-  ( A e. CC -> ( exp ` ( -u _i x. -u A ) ) = ( exp ` ( _i x. A ) ) )
30 26 29 oveq12d 
 |-  ( A e. CC -> ( ( exp ` ( _i x. -u A ) ) - ( exp ` ( -u _i x. -u A ) ) ) = ( ( exp ` ( -u _i x. A ) ) - ( exp ` ( _i x. A ) ) ) )
31 10 15 negsubdi2d 
 |-  ( A e. CC -> -u ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) = ( ( exp ` ( -u _i x. A ) ) - ( exp ` ( _i x. A ) ) ) )
32 30 31 eqtr4d 
 |-  ( A e. CC -> ( ( exp ` ( _i x. -u A ) ) - ( exp ` ( -u _i x. -u A ) ) ) = -u ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) )
33 32 oveq1d 
 |-  ( A e. CC -> ( ( ( exp ` ( _i x. -u A ) ) - ( exp ` ( -u _i x. -u A ) ) ) / ( 2 x. _i ) ) = ( -u ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( 2 x. _i ) ) )
34 22 33 eqtr4d 
 |-  ( A e. CC -> -u ( sin ` A ) = ( ( ( exp ` ( _i x. -u A ) ) - ( exp ` ( -u _i x. -u A ) ) ) / ( 2 x. _i ) ) )
35 3 34 eqtr4d 
 |-  ( A e. CC -> ( sin ` -u A ) = -u ( sin ` A ) )