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 2t1e2 ⊢ ( 2 · 1 ) = 2
2 df-2 ⊢ 2 = ( 1 + 1 )
3 1 2 eqtr2i ⊢ ( 1 + 1 ) = ( 2 · 1 )
4 zcn ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
5 2cn ⊢ 2 ∈ ℂ
6 picn ⊢ π ∈ ℂ
7 mul12 ⊢ ( ( 𝐾 ∈ ℂ ∧ 2 ∈ ℂ ∧ π ∈ ℂ ) → ( 𝐾 · ( 2 · π ) ) = ( 2 · ( 𝐾 · π ) ) )
8 5 6 7 mp3an23 ⊢ ( 𝐾 ∈ ℂ → ( 𝐾 · ( 2 · π ) ) = ( 2 · ( 𝐾 · π ) ) )
9 4 8 syl ⊢ ( 𝐾 ∈ ℤ → ( 𝐾 · ( 2 · π ) ) = ( 2 · ( 𝐾 · π ) ) )
10 9 fveq2d ⊢ ( 𝐾 ∈ ℤ → ( cos ‘ ( 𝐾 · ( 2 · π ) ) ) = ( cos ‘ ( 2 · ( 𝐾 · π ) ) ) )
11 cos2kpi ⊢ ( 𝐾 ∈ ℤ → ( cos ‘ ( 𝐾 · ( 2 · π ) ) ) = 1 )
12 zre ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
13 pire ⊢ π ∈ ℝ
14 remulcl ⊢ ( ( 𝐾 ∈ ℝ ∧ π ∈ ℝ ) → ( 𝐾 · π ) ∈ ℝ )
15 12 13 14 sylancl ⊢ ( 𝐾 ∈ ℤ → ( 𝐾 · π ) ∈ ℝ )
16 15 recnd ⊢ ( 𝐾 ∈ ℤ → ( 𝐾 · π ) ∈ ℂ )
17 cos2t ⊢ ( ( 𝐾 · π ) ∈ ℂ → ( cos ‘ ( 2 · ( 𝐾 · π ) ) ) = ( ( 2 · ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ) − 1 ) )
18 16 17 syl ⊢ ( 𝐾 ∈ ℤ → ( cos ‘ ( 2 · ( 𝐾 · π ) ) ) = ( ( 2 · ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ) − 1 ) )
19 10 11 18 3eqtr3rd ⊢ ( 𝐾 ∈ ℤ → ( ( 2 · ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ) − 1 ) = 1 )
20 15 recoscld ⊢ ( 𝐾 ∈ ℤ → ( cos ‘ ( 𝐾 · π ) ) ∈ ℝ )
21 20 recnd ⊢ ( 𝐾 ∈ ℤ → ( cos ‘ ( 𝐾 · π ) ) ∈ ℂ )
22 21 sqcld ⊢ ( 𝐾 ∈ ℤ → ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ∈ ℂ )
23 mulcl ⊢ ( ( 2 ∈ ℂ ∧ ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ∈ ℂ ) → ( 2 · ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ) ∈ ℂ )
24 5 22 23 sylancr ⊢ ( 𝐾 ∈ ℤ → ( 2 · ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ) ∈ ℂ )
25 ax-1cn ⊢ 1 ∈ ℂ
26 subadd ⊢ ( ( ( 2 · ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ) ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 2 · ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ) − 1 ) = 1 ↔ ( 1 + 1 ) = ( 2 · ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ) ) )
27 25 25 26 mp3an23 ⊢ ( ( 2 · ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ) ∈ ℂ → ( ( ( 2 · ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ) − 1 ) = 1 ↔ ( 1 + 1 ) = ( 2 · ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ) ) )
28 24 27 syl ⊢ ( 𝐾 ∈ ℤ → ( ( ( 2 · ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ) − 1 ) = 1 ↔ ( 1 + 1 ) = ( 2 · ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ) ) )
29 19 28 mpbid ⊢ ( 𝐾 ∈ ℤ → ( 1 + 1 ) = ( 2 · ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ) )
30 3 29 syl5reqr ⊢ ( 𝐾 ∈ ℤ → ( 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 25 31 32 mp3an23 ⊢ ( ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ∈ ℂ → ( ( 2 · ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) ) = ( 2 · 1 ) ↔ ( ( cos ‘ ( 𝐾 · π ) ) ↑ 2 ) = 1 ) )
34 22 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 20 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 syl6eq ⊢ ( 𝐾 ∈ ℤ → ( abs ‘ ( cos ‘ ( 𝐾 · π ) ) ) = 1 )