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 cos K 2 π = 1

Proof

Step Hyp Ref Expression
1 zcn K K
2 2cn 2
3 picn π
4 2 3 mulcli 2 π
5 mulcl K 2 π K 2 π
6 1 4 5 sylancl K K 2 π
7 6 addid2d K 0 + K 2 π = K 2 π
8 7 fveq2d K cos 0 + K 2 π = cos K 2 π
9 0cn 0
10 cosper 0 K cos 0 + K 2 π = cos 0
11 9 10 mpan K cos 0 + K 2 π = cos 0
12 cos0 cos 0 = 1
13 11 12 eqtrdi K cos 0 + K 2 π = 1
14 8 13 eqtr3d K cos K 2 π = 1