Metamath Proof Explorer

Theorem coskpi2

Description: The cosine of an integer multiple of negative _pi is either 1 or negative 1 . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion coskpi2 ( 𝐾 ∈ ℤ → ( cos ‘ ( 𝐾 · π ) ) = if ( 2 ∥ 𝐾 , 1 , - 1 ) )

Proof

Step Hyp Ref Expression
1 2z ⊢ 2 ∈ ℤ
2 divides ⊢ ( ( 2 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 2 ∥ 𝐾 ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 · 2 ) = 𝐾 ) )
3 1 2 mpan ⊢ ( 𝐾 ∈ ℤ → ( 2 ∥ 𝐾 ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 · 2 ) = 𝐾 ) )
4 3 biimpa ⊢ ( ( 𝐾 ∈ ℤ ∧ 2 ∥ 𝐾 ) → ∃ 𝑛 ∈ ℤ ( 𝑛 · 2 ) = 𝐾 )
5 zcn ⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℂ )
6 2cnd ⊢ ( 𝑛 ∈ ℤ → 2 ∈ ℂ )
7 picn ⊢ π ∈ ℂ
8 7 a1i ⊢ ( 𝑛 ∈ ℤ → π ∈ ℂ )
9 5 6 8 mulassd ⊢ ( 𝑛 ∈ ℤ → ( ( 𝑛 · 2 ) · π ) = ( 𝑛 · ( 2 · π ) ) )
10 9 eqcomd ⊢ ( 𝑛 ∈ ℤ → ( 𝑛 · ( 2 · π ) ) = ( ( 𝑛 · 2 ) · π ) )
11 10 adantr ⊢ ( ( 𝑛 ∈ ℤ ∧ ( 𝑛 · 2 ) = 𝐾 ) → ( 𝑛 · ( 2 · π ) ) = ( ( 𝑛 · 2 ) · π ) )
12 oveq1 ⊢ ( ( 𝑛 · 2 ) = 𝐾 → ( ( 𝑛 · 2 ) · π ) = ( 𝐾 · π ) )
13 12 adantl ⊢ ( ( 𝑛 ∈ ℤ ∧ ( 𝑛 · 2 ) = 𝐾 ) → ( ( 𝑛 · 2 ) · π ) = ( 𝐾 · π ) )
14 11 13 eqtr2d ⊢ ( ( 𝑛 ∈ ℤ ∧ ( 𝑛 · 2 ) = 𝐾 ) → ( 𝐾 · π ) = ( 𝑛 · ( 2 · π ) ) )
15 14 fveq2d ⊢ ( ( 𝑛 ∈ ℤ ∧ ( 𝑛 · 2 ) = 𝐾 ) → ( cos ‘ ( 𝐾 · π ) ) = ( cos ‘ ( 𝑛 · ( 2 · π ) ) ) )
16 cos2kpi ⊢ ( 𝑛 ∈ ℤ → ( cos ‘ ( 𝑛 · ( 2 · π ) ) ) = 1 )
17 16 adantr ⊢ ( ( 𝑛 ∈ ℤ ∧ ( 𝑛 · 2 ) = 𝐾 ) → ( cos ‘ ( 𝑛 · ( 2 · π ) ) ) = 1 )
18 15 17 eqtrd ⊢ ( ( 𝑛 ∈ ℤ ∧ ( 𝑛 · 2 ) = 𝐾 ) → ( cos ‘ ( 𝐾 · π ) ) = 1 )
19 18 3adant1 ⊢ ( ( 2 ∥ 𝐾 ∧ 𝑛 ∈ ℤ ∧ ( 𝑛 · 2 ) = 𝐾 ) → ( cos ‘ ( 𝐾 · π ) ) = 1 )
20 iftrue ⊢ ( 2 ∥ 𝐾 → if ( 2 ∥ 𝐾 , 1 , - 1 ) = 1 )
21 20 eqcomd ⊢ ( 2 ∥ 𝐾 → 1 = if ( 2 ∥ 𝐾 , 1 , - 1 ) )
22 21 3ad2ant1 ⊢ ( ( 2 ∥ 𝐾 ∧ 𝑛 ∈ ℤ ∧ ( 𝑛 · 2 ) = 𝐾 ) → 1 = if ( 2 ∥ 𝐾 , 1 , - 1 ) )
23 19 22 eqtrd ⊢ ( ( 2 ∥ 𝐾 ∧ 𝑛 ∈ ℤ ∧ ( 𝑛 · 2 ) = 𝐾 ) → ( cos ‘ ( 𝐾 · π ) ) = if ( 2 ∥ 𝐾 , 1 , - 1 ) )
24 23 3exp ⊢ ( 2 ∥ 𝐾 → ( 𝑛 ∈ ℤ → ( ( 𝑛 · 2 ) = 𝐾 → ( cos ‘ ( 𝐾 · π ) ) = if ( 2 ∥ 𝐾 , 1 , - 1 ) ) ) )
25 24 adantl ⊢ ( ( 𝐾 ∈ ℤ ∧ 2 ∥ 𝐾 ) → ( 𝑛 ∈ ℤ → ( ( 𝑛 · 2 ) = 𝐾 → ( cos ‘ ( 𝐾 · π ) ) = if ( 2 ∥ 𝐾 , 1 , - 1 ) ) ) )
26 25 rexlimdv ⊢ ( ( 𝐾 ∈ ℤ ∧ 2 ∥ 𝐾 ) → ( ∃ 𝑛 ∈ ℤ ( 𝑛 · 2 ) = 𝐾 → ( cos ‘ ( 𝐾 · π ) ) = if ( 2 ∥ 𝐾 , 1 , - 1 ) ) )
27 4 26 mpd ⊢ ( ( 𝐾 ∈ ℤ ∧ 2 ∥ 𝐾 ) → ( cos ‘ ( 𝐾 · π ) ) = if ( 2 ∥ 𝐾 , 1 , - 1 ) )
28 odd2np1 ⊢ ( 𝐾 ∈ ℤ → ( ¬ 2 ∥ 𝐾 ↔ ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝐾 ) )
29 28 biimpa ⊢ ( ( 𝐾 ∈ ℤ ∧ ¬ 2 ∥ 𝐾 ) → ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝐾 )
30 6 5 mulcld ⊢ ( 𝑛 ∈ ℤ → ( 2 · 𝑛 ) ∈ ℂ )
31 1cnd ⊢ ( 𝑛 ∈ ℤ → 1 ∈ ℂ )
32 30 31 8 adddird ⊢ ( 𝑛 ∈ ℤ → ( ( ( 2 · 𝑛 ) + 1 ) · π ) = ( ( ( 2 · 𝑛 ) · π ) + ( 1 · π ) ) )
33 6 5 mulcomd ⊢ ( 𝑛 ∈ ℤ → ( 2 · 𝑛 ) = ( 𝑛 · 2 ) )
34 33 oveq1d ⊢ ( 𝑛 ∈ ℤ → ( ( 2 · 𝑛 ) · π ) = ( ( 𝑛 · 2 ) · π ) )
35 34 9 eqtrd ⊢ ( 𝑛 ∈ ℤ → ( ( 2 · 𝑛 ) · π ) = ( 𝑛 · ( 2 · π ) ) )
36 7 mulid2i ⊢ ( 1 · π ) = π
37 36 a1i ⊢ ( 𝑛 ∈ ℤ → ( 1 · π ) = π )
38 35 37 oveq12d ⊢ ( 𝑛 ∈ ℤ → ( ( ( 2 · 𝑛 ) · π ) + ( 1 · π ) ) = ( ( 𝑛 · ( 2 · π ) ) + π ) )
39 2cn ⊢ 2 ∈ ℂ
40 39 7 mulcli ⊢ ( 2 · π ) ∈ ℂ
41 40 a1i ⊢ ( 𝑛 ∈ ℤ → ( 2 · π ) ∈ ℂ )
42 5 41 mulcld ⊢ ( 𝑛 ∈ ℤ → ( 𝑛 · ( 2 · π ) ) ∈ ℂ )
43 42 8 addcomd ⊢ ( 𝑛 ∈ ℤ → ( ( 𝑛 · ( 2 · π ) ) + π ) = ( π + ( 𝑛 · ( 2 · π ) ) ) )
44 32 38 43 3eqtrrd ⊢ ( 𝑛 ∈ ℤ → ( π + ( 𝑛 · ( 2 · π ) ) ) = ( ( ( 2 · 𝑛 ) + 1 ) · π ) )
45 44 adantr ⊢ ( ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝐾 ) → ( π + ( 𝑛 · ( 2 · π ) ) ) = ( ( ( 2 · 𝑛 ) + 1 ) · π ) )
46 oveq1 ⊢ ( ( ( 2 · 𝑛 ) + 1 ) = 𝐾 → ( ( ( 2 · 𝑛 ) + 1 ) · π ) = ( 𝐾 · π ) )
47 46 adantl ⊢ ( ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝐾 ) → ( ( ( 2 · 𝑛 ) + 1 ) · π ) = ( 𝐾 · π ) )
48 45 47 eqtr2d ⊢ ( ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝐾 ) → ( 𝐾 · π ) = ( π + ( 𝑛 · ( 2 · π ) ) ) )
49 48 fveq2d ⊢ ( ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝐾 ) → ( cos ‘ ( 𝐾 · π ) ) = ( cos ‘ ( π + ( 𝑛 · ( 2 · π ) ) ) ) )
50 cosper ⊢ ( ( π ∈ ℂ ∧ 𝑛 ∈ ℤ ) → ( cos ‘ ( π + ( 𝑛 · ( 2 · π ) ) ) ) = ( cos ‘ π ) )
51 7 50 mpan ⊢ ( 𝑛 ∈ ℤ → ( cos ‘ ( π + ( 𝑛 · ( 2 · π ) ) ) ) = ( cos ‘ π ) )
52 51 adantr ⊢ ( ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝐾 ) → ( cos ‘ ( π + ( 𝑛 · ( 2 · π ) ) ) ) = ( cos ‘ π ) )
53 cospi ⊢ ( cos ‘ π ) = - 1
54 53 a1i ⊢ ( ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝐾 ) → ( cos ‘ π ) = - 1 )
55 49 52 54 3eqtrd ⊢ ( ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝐾 ) → ( cos ‘ ( 𝐾 · π ) ) = - 1 )
56 55 3adant1 ⊢ ( ( ¬ 2 ∥ 𝐾 ∧ 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝐾 ) → ( cos ‘ ( 𝐾 · π ) ) = - 1 )
57 iffalse ⊢ ( ¬ 2 ∥ 𝐾 → if ( 2 ∥ 𝐾 , 1 , - 1 ) = - 1 )
58 57 eqcomd ⊢ ( ¬ 2 ∥ 𝐾 → - 1 = if ( 2 ∥ 𝐾 , 1 , - 1 ) )
59 58 3ad2ant1 ⊢ ( ( ¬ 2 ∥ 𝐾 ∧ 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝐾 ) → - 1 = if ( 2 ∥ 𝐾 , 1 , - 1 ) )
60 56 59 eqtrd ⊢ ( ( ¬ 2 ∥ 𝐾 ∧ 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝐾 ) → ( cos ‘ ( 𝐾 · π ) ) = if ( 2 ∥ 𝐾 , 1 , - 1 ) )
61 60 3exp ⊢ ( ¬ 2 ∥ 𝐾 → ( 𝑛 ∈ ℤ → ( ( ( 2 · 𝑛 ) + 1 ) = 𝐾 → ( cos ‘ ( 𝐾 · π ) ) = if ( 2 ∥ 𝐾 , 1 , - 1 ) ) ) )
62 61 adantl ⊢ ( ( 𝐾 ∈ ℤ ∧ ¬ 2 ∥ 𝐾 ) → ( 𝑛 ∈ ℤ → ( ( ( 2 · 𝑛 ) + 1 ) = 𝐾 → ( cos ‘ ( 𝐾 · π ) ) = if ( 2 ∥ 𝐾 , 1 , - 1 ) ) ) )
63 62 rexlimdv ⊢ ( ( 𝐾 ∈ ℤ ∧ ¬ 2 ∥ 𝐾 ) → ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝐾 → ( cos ‘ ( 𝐾 · π ) ) = if ( 2 ∥ 𝐾 , 1 , - 1 ) ) )
64 29 63 mpd ⊢ ( ( 𝐾 ∈ ℤ ∧ ¬ 2 ∥ 𝐾 ) → ( cos ‘ ( 𝐾 · π ) ) = if ( 2 ∥ 𝐾 , 1 , - 1 ) )
65 27 64 pm2.61dan ⊢ ( 𝐾 ∈ ℤ → ( cos ‘ ( 𝐾 · π ) ) = if ( 2 ∥ 𝐾 , 1 , - 1 ) )