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

Proof

Step	Hyp	Ref	Expression
1		zcn	⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
2		2cn	⊢ 2 ∈ ℂ
3		picn	⊢ π ∈ ℂ
4		mul12	⊢ ( ( 𝐾 ∈ ℂ ∧ 2 ∈ ℂ ∧ π ∈ ℂ ) → ( 𝐾 · ( 2 · π ) ) = ( 2 · ( 𝐾 · π ) ) )
5	2 3 4	mp3an23	⊢ ( 𝐾 ∈ ℂ → ( 𝐾 · ( 2 · π ) ) = ( 2 · ( 𝐾 · π ) ) )
6	1 5	syl	⊢ ( 𝐾 ∈ ℤ → ( 𝐾 · ( 2 · π ) ) = ( 2 · ( 𝐾 · π ) ) )
7	6	fveq2d	⊢ ( 𝐾 ∈ ℤ → ( cos ‘ ( 𝐾 · ( 2 · π ) ) ) = ( cos ‘ ( 2 · ( 𝐾 · π ) ) ) )
8		cos2kpi	⊢ ( 𝐾 ∈ ℤ → ( cos ‘ ( 𝐾 · ( 2 · π ) ) ) = 1 )
9		zre	⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
10		pire	⊢ π ∈ ℝ
11		remulcl	⊢ ( ( 𝐾 ∈ ℝ ∧ π ∈ ℝ ) → ( 𝐾 · π ) ∈ ℝ )
12	9 10 11	sylancl	⊢ ( 𝐾 ∈ ℤ → ( 𝐾 · π ) ∈ ℝ )
13	12	recnd	⊢ ( 𝐾 ∈ ℤ → ( 𝐾 · π ) ∈ ℂ )
14		cos2t	⊢ ( ( 𝐾 · π ) ∈ ℂ → ( cos ‘ ( 2 · ( 𝐾 · π ) ) ) = ( ( 2 · ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ) − 1 ) )
15	13 14	syl	⊢ ( 𝐾 ∈ ℤ → ( cos ‘ ( 2 · ( 𝐾 · π ) ) ) = ( ( 2 · ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ) − 1 ) )
16	7 8 15	3eqtr3rd	⊢ ( 𝐾 ∈ ℤ → ( ( 2 · ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ) − 1 ) = 1 )
17	12	recoscld	⊢ ( 𝐾 ∈ ℤ → ( cos ‘ ( 𝐾 · π ) ) ∈ ℝ )
18	17	recnd	⊢ ( 𝐾 ∈ ℤ → ( cos ‘ ( 𝐾 · π ) ) ∈ ℂ )
19	18	sqcld	⊢ ( 𝐾 ∈ ℤ → ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ∈ ℂ )
20		mulcl	⊢ ( ( 2 ∈ ℂ ∧ ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ∈ ℂ ) → ( 2 · ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ) ∈ ℂ )
21	2 19 20	sylancr	⊢ ( 𝐾 ∈ ℤ → ( 2 · ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ) ∈ ℂ )
22		ax-1cn	⊢ 1 ∈ ℂ
23		subadd	⊢ ( ( ( 2 · ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ) ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 2 · ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ) − 1 ) = 1 ↔ ( 1 + 1 ) = ( 2 · ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ) ) )
24	22 22 23	mp3an23	⊢ ( ( 2 · ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ) ∈ ℂ → ( ( ( 2 · ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ) − 1 ) = 1 ↔ ( 1 + 1 ) = ( 2 · ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ) ) )
25	21 24	syl	⊢ ( 𝐾 ∈ ℤ → ( ( ( 2 · ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ) − 1 ) = 1 ↔ ( 1 + 1 ) = ( 2 · ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ) ) )
26	16 25	mpbid	⊢ ( 𝐾 ∈ ℤ → ( 1 + 1 ) = ( 2 · ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ) )
27		2t1e2	⊢ ( 2 · 1 ) = 2
28		df-2	⊢ 2 = ( 1 + 1 )
29	27 28	eqtr2i	⊢ ( 1 + 1 ) = ( 2 · 1 )
30	26 29	eqtr3di	⊢ ( 𝐾 ∈ ℤ → ( 2 · ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ) = ( 2 · 1 ) )
31		2cnne0	⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
32		mulcan	⊢ ( ( ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( 2 · ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ) = ( 2 · 1 ) ↔ ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) = 1 ) )
33	22 31 32	mp3an23	⊢ ( ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ∈ ℂ → ( ( 2 · ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ) = ( 2 · 1 ) ↔ ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) = 1 ) )
34	19 33	syl	⊢ ( 𝐾 ∈ ℤ → ( ( 2 · ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ) = ( 2 · 1 ) ↔ ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) = 1 ) )
35	30 34	mpbid	⊢ ( 𝐾 ∈ ℤ → ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) = 1 )
36		sq1	⊢ ( 1 ↑ 2 ) = 1
37	35 36	eqtr4di	⊢ ( 𝐾 ∈ ℤ → ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) = ( 1 ↑ 2 ) )
38		1re	⊢ 1 ∈ ℝ
39		sqabs	⊢ ( ( ( cos ‘ ( 𝐾 · π ) ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) = ( 1 ↑ 2 ) ↔ ( abs ‘ ( cos ‘ ( 𝐾 · π ) ) ) = ( abs ‘ 1 ) ) )
40	17 38 39	sylancl	⊢ ( 𝐾 ∈ ℤ → ( ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) = ( 1 ↑ 2 ) ↔ ( abs ‘ ( cos ‘ ( 𝐾 · π ) ) ) = ( abs ‘ 1 ) ) )
41	37 40	mpbid	⊢ ( 𝐾 ∈ ℤ → ( abs ‘ ( cos ‘ ( 𝐾 · π ) ) ) = ( abs ‘ 1 ) )
42		abs1	⊢ ( abs ‘ 1 ) = 1
43	41 42	eqtrdi	⊢ ( 𝐾 ∈ ℤ → ( abs ‘ ( cos ‘ ( 𝐾 · π ) ) ) = 1 )