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 ( 𝐾 ∈ ℤ → ( cos ‘ ( 𝐾 · ( 2 · π ) ) ) = 1 )

Proof

Step Hyp Ref Expression
1 zcn ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
2 2cn ⊢ 2 ∈ ℂ
3 picn ⊢ π ∈ ℂ
4 2 3 mulcli ⊢ ( 2 · π ) ∈ ℂ
5 mulcl ⊢ ( ( 𝐾 ∈ ℂ ∧ ( 2 · π ) ∈ ℂ ) → ( 𝐾 · ( 2 · π ) ) ∈ ℂ )
6 1 4 5 sylancl ⊢ ( 𝐾 ∈ ℤ → ( 𝐾 · ( 2 · π ) ) ∈ ℂ )
7 6 addlidd ⊢ ( 𝐾 ∈ ℤ → ( 0 + ( 𝐾 · ( 2 · π ) ) ) = ( 𝐾 · ( 2 · π ) ) )
8 7 fveq2d ⊢ ( 𝐾 ∈ ℤ → ( cos ‘ ( 0 + ( 𝐾 · ( 2 · π ) ) ) ) = ( cos ‘ ( 𝐾 · ( 2 · π ) ) ) )
9 0cn ⊢ 0 ∈ ℂ
10 cosper ⊢ ( ( 0 ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( cos ‘ ( 0 + ( 𝐾 · ( 2 · π ) ) ) ) = ( cos ‘ 0 ) )
11 9 10 mpan ⊢ ( 𝐾 ∈ ℤ → ( cos ‘ ( 0 + ( 𝐾 · ( 2 · π ) ) ) ) = ( cos ‘ 0 ) )
12 cos0 ⊢ ( cos ‘ 0 ) = 1
13 11 12 eqtrdi ⊢ ( 𝐾 ∈ ℤ → ( cos ‘ ( 0 + ( 𝐾 · ( 2 · π ) ) ) ) = 1 )
14 8 13 eqtr3d ⊢ ( 𝐾 ∈ ℤ → ( cos ‘ ( 𝐾 · ( 2 · π ) ) ) = 1 )