coskpi

Description: The absolute value of the cosine of an integer multiple of _pi is 1. (Contributed by NM, 19-Aug-2008)

		Ref	Expression
	Assertion	coskpi	$⊢ K \in ℤ \to \|\cos K π\| = 1$

Proof

Step	Hyp	Ref	Expression
1		zcn	$⊢ K \in ℤ \to K \in ℂ$
2		2cn	$⊢ 2 \in ℂ$
3		picn	$⊢ π \in ℂ$
4		mul12	$⊢ (K \in ℂ \land 2 \in ℂ \land π \in ℂ) \to K 2 π = 2 K π$
5	2 3 4	mp3an23	$⊢ K \in ℂ \to K 2 π = 2 K π$
6	1 5	syl	$⊢ K \in ℤ \to K 2 π = 2 K π$
7	6	fveq2d	$⊢ K \in ℤ \to \cos K 2 π = \cos 2 K π$
8		cos2kpi	$⊢ K \in ℤ \to \cos K 2 π = 1$
9		zre	$⊢ K \in ℤ \to K \in ℝ$
10		pire	$⊢ π \in ℝ$
11		remulcl	$⊢ (K \in ℝ \land π \in ℝ) \to K π \in ℝ$
12	9 10 11	sylancl	$⊢ K \in ℤ \to K π \in ℝ$
13	12	recnd	$⊢ K \in ℤ \to K π \in ℂ$
14		cos2t	$⊢ K π \in ℂ \to \cos 2 K π = 2 {\cos K π}^{2} - 1$
15	13 14	syl	$⊢ K \in ℤ \to \cos 2 K π = 2 {\cos K π}^{2} - 1$
16	7 8 15	3eqtr3rd	$⊢ K \in ℤ \to 2 {\cos K π}^{2} - 1 = 1$
17	12	recoscld	$⊢ K \in ℤ \to \cos K π \in ℝ$
18	17	recnd	$⊢ K \in ℤ \to \cos K π \in ℂ$
19	18	sqcld	$⊢ K \in ℤ \to {\cos K π}^{2} \in ℂ$
20		mulcl	$⊢ (2 \in ℂ \land {\cos K π}^{2} \in ℂ) \to 2 {\cos K π}^{2} \in ℂ$
21	2 19 20	sylancr	$⊢ K \in ℤ \to 2 {\cos K π}^{2} \in ℂ$
22		ax-1cn	$⊢ 1 \in ℂ$
23		subadd	$⊢ (2 {\cos K π}^{2} \in ℂ \land 1 \in ℂ \land 1 \in ℂ) \to (2 {\cos K π}^{2} - 1 = 1 \leftrightarrow 1 + 1 = 2 {\cos K π}^{2})$
24	22 22 23	mp3an23	$⊢ 2 {\cos K π}^{2} \in ℂ \to (2 {\cos K π}^{2} - 1 = 1 \leftrightarrow 1 + 1 = 2 {\cos K π}^{2})$
25	21 24	syl	$⊢ K \in ℤ \to (2 {\cos K π}^{2} - 1 = 1 \leftrightarrow 1 + 1 = 2 {\cos K π}^{2})$
26	16 25	mpbid	$⊢ K \in ℤ \to 1 + 1 = 2 {\cos K π}^{2}$
27		2t1e2	$⊢ 2 \cdot 1 = 2$
28		df-2	$⊢ 2 = 1 + 1$
29	27 28	eqtr2i	$⊢ 1 + 1 = 2 \cdot 1$
30	26 29	eqtr3di	$⊢ K \in ℤ \to 2 {\cos K π}^{2} = 2 \cdot 1$
31		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
32		mulcan	$⊢ ({\cos K π}^{2} \in ℂ \land 1 \in ℂ \land (2 \in ℂ \land 2 \neq 0)) \to (2 {\cos K π}^{2} = 2 \cdot 1 \leftrightarrow {\cos K π}^{2} = 1)$
33	22 31 32	mp3an23	$⊢ {\cos K π}^{2} \in ℂ \to (2 {\cos K π}^{2} = 2 \cdot 1 \leftrightarrow {\cos K π}^{2} = 1)$
34	19 33	syl	$⊢ K \in ℤ \to (2 {\cos K π}^{2} = 2 \cdot 1 \leftrightarrow {\cos K π}^{2} = 1)$
35	30 34	mpbid	$⊢ K \in ℤ \to {\cos K π}^{2} = 1$
36		sq1	$⊢ 1^{2} = 1$
37	35 36	eqtr4di	$⊢ K \in ℤ \to {\cos K π}^{2} = 1^{2}$
38		1re	$⊢ 1 \in ℝ$
39		sqabs	$⊢ (\cos K π \in ℝ \land 1 \in ℝ) \to ({\cos K π}^{2} = 1^{2} \leftrightarrow \|\cos K π\| = \|1\|)$
40	17 38 39	sylancl	$⊢ K \in ℤ \to ({\cos K π}^{2} = 1^{2} \leftrightarrow \|\cos K π\| = \|1\|)$
41	37 40	mpbid	$⊢ K \in ℤ \to \|\cos K π\| = \|1\|$
42		abs1	$⊢ \|1\| = 1$
43	41 42	eqtrdi	$⊢ K \in ℤ \to \|\cos K π\| = 1$

Metamath Proof Explorer

Theorem coskpi

Proof