Metamath Proof Explorer

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 )