This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cos2kpi

Description: If K is an integer, then the cosine of 2 K _pi is 1. (Contributed by Paul Chapman, 23-Jan-2008) (Revised by Mario Carneiro, 10-May-2014)

Ref Expression
Assertion cos2kpi 
|- ( K e. ZZ -> ( cos ` ( K x. ( 2 x. _pi ) ) ) = 1 )

Proof

Step Hyp Ref Expression
1 zcn 
 |-  ( K e. ZZ -> K e. CC )
2 2cn 
 |-  2 e. CC
3 picn 
 |-  _pi e. CC
4 2 3 mulcli 
 |-  ( 2 x. _pi ) e. CC
5 mulcl 
 |-  ( ( K e. CC /\ ( 2 x. _pi ) e. CC ) -> ( K x. ( 2 x. _pi ) ) e. CC )
6 1 4 5 sylancl 
 |-  ( K e. ZZ -> ( K x. ( 2 x. _pi ) ) e. CC )
7 6 addlidd 
 |-  ( K e. ZZ -> ( 0 + ( K x. ( 2 x. _pi ) ) ) = ( K x. ( 2 x. _pi ) ) )
8 7 fveq2d 
 |-  ( K e. ZZ -> ( cos ` ( 0 + ( K x. ( 2 x. _pi ) ) ) ) = ( cos ` ( K x. ( 2 x. _pi ) ) ) )
9 0cn 
 |-  0 e. CC
10 cosper 
 |-  ( ( 0 e. CC /\ K e. ZZ ) -> ( cos ` ( 0 + ( K x. ( 2 x. _pi ) ) ) ) = ( cos ` 0 ) )
11 9 10 mpan 
 |-  ( K e. ZZ -> ( cos ` ( 0 + ( K x. ( 2 x. _pi ) ) ) ) = ( cos ` 0 ) )
12 cos0 
 |-  ( cos ` 0 ) = 1
13 11 12 eqtrdi 
 |-  ( K e. ZZ -> ( cos ` ( 0 + ( K x. ( 2 x. _pi ) ) ) ) = 1 )
14 8 13 eqtr3d 
 |-  ( K e. ZZ -> ( cos ` ( K x. ( 2 x. _pi ) ) ) = 1 )