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		2t1e2	$⊢ 2 \cdot 1 = 2$
2		df-2	$⊢ 2 = 1 + 1$
3	1 2	eqtr2i	$⊢ 1 + 1 = 2 \cdot 1$
4		zcn	$⊢ K \in ℤ \to K \in ℂ$
5		2cn	$⊢ 2 \in ℂ$
6		picn	$⊢ π \in ℂ$
7		mul12	$⊢ (K \in ℂ \land 2 \in ℂ \land π \in ℂ) \to K 2 π = 2 K π$
8	5 6 7	mp3an23	$⊢ K \in ℂ \to K 2 π = 2 K π$
9	4 8	syl	$⊢ K \in ℤ \to K 2 π = 2 K π$
10	9	fveq2d	$⊢ K \in ℤ \to \cos K 2 π = \cos 2 K π$
11		cos2kpi	$⊢ K \in ℤ \to \cos K 2 π = 1$
12		zre	$⊢ K \in ℤ \to K \in ℝ$
13		pire	$⊢ π \in ℝ$
14		remulcl	$⊢ (K \in ℝ \land π \in ℝ) \to K π \in ℝ$
15	12 13 14	sylancl	$⊢ K \in ℤ \to K π \in ℝ$
16	15	recnd	$⊢ K \in ℤ \to K π \in ℂ$
17		cos2t	$⊢ K π \in ℂ \to \cos 2 K π = 2 {\cos K π}^{2} - 1$
18	16 17	syl	$⊢ K \in ℤ \to \cos 2 K π = 2 {\cos K π}^{2} - 1$
19	10 11 18	3eqtr3rd	$⊢ K \in ℤ \to 2 {\cos K π}^{2} - 1 = 1$
20	15	recoscld	$⊢ K \in ℤ \to \cos K π \in ℝ$
21	20	recnd	$⊢ K \in ℤ \to \cos K π \in ℂ$
22	21	sqcld	$⊢ K \in ℤ \to {\cos K π}^{2} \in ℂ$
23		mulcl	$⊢ (2 \in ℂ \land {\cos K π}^{2} \in ℂ) \to 2 {\cos K π}^{2} \in ℂ$
24	5 22 23	sylancr	$⊢ K \in ℤ \to 2 {\cos K π}^{2} \in ℂ$
25		ax-1cn	$⊢ 1 \in ℂ$
26		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})$
27	25 25 26	mp3an23	$⊢ 2 {\cos K π}^{2} \in ℂ \to (2 {\cos K π}^{2} - 1 = 1 \leftrightarrow 1 + 1 = 2 {\cos K π}^{2})$
28	24 27	syl	$⊢ K \in ℤ \to (2 {\cos K π}^{2} - 1 = 1 \leftrightarrow 1 + 1 = 2 {\cos K π}^{2})$
29	19 28	mpbid	$⊢ K \in ℤ \to 1 + 1 = 2 {\cos K π}^{2}$
30	3 29	syl5reqr	$⊢ 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	25 31 32	mp3an23	$⊢ {\cos K π}^{2} \in ℂ \to (2 {\cos K π}^{2} = 2 \cdot 1 \leftrightarrow {\cos K π}^{2} = 1)$
34	22 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	20 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	syl6eq	$⊢ K \in ℤ \to \|\cos K π\| = 1$

Metamath Proof Explorer

Theorem coskpi

Proof