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