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 )