Metamath Proof Explorer


Theorem sin2pim

Description: Sine of a number subtracted from 2 x. _pi . (Contributed by Paul Chapman, 15-Mar-2008)

Ref Expression
Assertion sin2pim
|- ( A e. CC -> ( sin ` ( ( 2 x. _pi ) - A ) ) = -u ( sin ` A ) )

Proof

Step Hyp Ref Expression
1 negcl
 |-  ( A e. CC -> -u A e. CC )
2 1z
 |-  1 e. ZZ
3 sinper
 |-  ( ( -u A e. CC /\ 1 e. ZZ ) -> ( sin ` ( -u A + ( 1 x. ( 2 x. _pi ) ) ) ) = ( sin ` -u A ) )
4 1 2 3 sylancl
 |-  ( A e. CC -> ( sin ` ( -u A + ( 1 x. ( 2 x. _pi ) ) ) ) = ( sin ` -u A ) )
5 2cn
 |-  2 e. CC
6 picn
 |-  _pi e. CC
7 5 6 mulcli
 |-  ( 2 x. _pi ) e. CC
8 7 mulid2i
 |-  ( 1 x. ( 2 x. _pi ) ) = ( 2 x. _pi )
9 8 oveq2i
 |-  ( -u A + ( 1 x. ( 2 x. _pi ) ) ) = ( -u A + ( 2 x. _pi ) )
10 negsubdi
 |-  ( ( A e. CC /\ ( 2 x. _pi ) e. CC ) -> -u ( A - ( 2 x. _pi ) ) = ( -u A + ( 2 x. _pi ) ) )
11 negsubdi2
 |-  ( ( A e. CC /\ ( 2 x. _pi ) e. CC ) -> -u ( A - ( 2 x. _pi ) ) = ( ( 2 x. _pi ) - A ) )
12 10 11 eqtr3d
 |-  ( ( A e. CC /\ ( 2 x. _pi ) e. CC ) -> ( -u A + ( 2 x. _pi ) ) = ( ( 2 x. _pi ) - A ) )
13 7 12 mpan2
 |-  ( A e. CC -> ( -u A + ( 2 x. _pi ) ) = ( ( 2 x. _pi ) - A ) )
14 9 13 syl5eq
 |-  ( A e. CC -> ( -u A + ( 1 x. ( 2 x. _pi ) ) ) = ( ( 2 x. _pi ) - A ) )
15 14 fveq2d
 |-  ( A e. CC -> ( sin ` ( -u A + ( 1 x. ( 2 x. _pi ) ) ) ) = ( sin ` ( ( 2 x. _pi ) - A ) ) )
16 4 15 eqtr3d
 |-  ( A e. CC -> ( sin ` -u A ) = ( sin ` ( ( 2 x. _pi ) - A ) ) )
17 sinneg
 |-  ( A e. CC -> ( sin ` -u A ) = -u ( sin ` A ) )
18 16 17 eqtr3d
 |-  ( A e. CC -> ( sin ` ( ( 2 x. _pi ) - A ) ) = -u ( sin ` A ) )