Metamath Proof Explorer

Theorem cos2pim

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

Ref Expression
Assertion cos2pim 
|- ( A e. CC -> ( cos ` ( ( 2 x. _pi ) - A ) ) = ( cos ` A ) )

Proof

Step Hyp Ref Expression
1 negcl 
 |-  ( A e. CC -> -u A e. CC )
2 1z 
 |-  1 e. ZZ
3 cosper 
 |-  ( ( -u A e. CC /\ 1 e. ZZ ) -> ( cos ` ( -u A + ( 1 x. ( 2 x. _pi ) ) ) ) = ( cos ` -u A ) )
4 1 2 3 sylancl 
 |-  ( A e. CC -> ( cos ` ( -u A + ( 1 x. ( 2 x. _pi ) ) ) ) = ( cos ` -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 -> ( cos ` ( -u A + ( 1 x. ( 2 x. _pi ) ) ) ) = ( cos ` ( ( 2 x. _pi ) - A ) ) )
16 4 15 eqtr3d 
 |-  ( A e. CC -> ( cos ` -u A ) = ( cos ` ( ( 2 x. _pi ) - A ) ) )
17 cosneg 
 |-  ( A e. CC -> ( cos ` -u A ) = ( cos ` A ) )
18 16 17 eqtr3d 
 |-  ( A e. CC -> ( cos ` ( ( 2 x. _pi ) - A ) ) = ( cos ` A ) )