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 \in ℤ \to \cos K 2 π = 1$

Proof

Step	Hyp	Ref	Expression
1		zcn	$⊢ K \in ℤ \to K \in ℂ$
2		2cn	$⊢ 2 \in ℂ$
3		picn	$⊢ π \in ℂ$
4	2 3	mulcli	$⊢ 2 π \in ℂ$
5		mulcl	$⊢ (K \in ℂ \land 2 π \in ℂ) \to K 2 π \in ℂ$
6	1 4 5	sylancl	$⊢ K \in ℤ \to K 2 π \in ℂ$
7	6	addlidd	$⊢ K \in ℤ \to 0 + K 2 π = K 2 π$
8	7	fveq2d	$⊢ K \in ℤ \to \cos (0 + K 2 π) = \cos K 2 π$
9		0cn	$⊢ 0 \in ℂ$
10		cosper	$⊢ (0 \in ℂ \land K \in ℤ) \to \cos (0 + K 2 π) = \cos 0$
11	9 10	mpan	$⊢ K \in ℤ \to \cos (0 + K 2 π) = \cos 0$
12		cos0	$⊢ \cos 0 = 1$
13	11 12	eqtrdi	$⊢ K \in ℤ \to \cos (0 + K 2 π) = 1$
14	8 13	eqtr3d	$⊢ K \in ℤ \to \cos K 2 π = 1$