Metamath Proof Explorer

Theorem cosknegpi

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 cosknegpi ( 𝐾 ∈ ℤ → ( cos ‘ ( 𝐾 · - π ) ) = if ( 2 ∥ 𝐾 , 1 , - 1 ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝐾 ∈ ℤ ∧ 2 ∥ 𝐾 ) → 2 ∥ 𝐾 )
2 2z ⊢ 2 ∈ ℤ
3 simpl ⊢ ( ( 𝐾 ∈ ℤ ∧ 2 ∥ 𝐾 ) → 𝐾 ∈ ℤ )
4 divides ⊢ ( ( 2 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 2 ∥ 𝐾 ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 · 2 ) = 𝐾 ) )
5 2 3 4 sylancr ⊢ ( ( 𝐾 ∈ ℤ ∧ 2 ∥ 𝐾 ) → ( 2 ∥ 𝐾 ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 · 2 ) = 𝐾 ) )
6 1 5 mpbid ⊢ ( ( 𝐾 ∈ ℤ ∧ 2 ∥ 𝐾 ) → ∃ 𝑛 ∈ ℤ ( 𝑛 · 2 ) = 𝐾 )
7 zcn ⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℂ )
8 negcl ⊢ ( 𝑛 ∈ ℂ → - 𝑛 ∈ ℂ )
9 2cn ⊢ 2 ∈ ℂ
10 picn ⊢ π ∈ ℂ
11 9 10 mulcli ⊢ ( 2 · π ) ∈ ℂ
12 11 a1i ⊢ ( 𝑛 ∈ ℂ → ( 2 · π ) ∈ ℂ )
13 8 12 mulcld ⊢ ( 𝑛 ∈ ℂ → ( - 𝑛 · ( 2 · π ) ) ∈ ℂ )
14 13 addid2d ⊢ ( 𝑛 ∈ ℂ → ( 0 + ( - 𝑛 · ( 2 · π ) ) ) = ( - 𝑛 · ( 2 · π ) ) )
15 2cnd ⊢ ( 𝑛 ∈ ℂ → 2 ∈ ℂ )
16 10 a1i ⊢ ( 𝑛 ∈ ℂ → π ∈ ℂ )
17 8 15 16 mulassd ⊢ ( 𝑛 ∈ ℂ → ( ( - 𝑛 · 2 ) · π ) = ( - 𝑛 · ( 2 · π ) ) )
18 17 eqcomd ⊢ ( 𝑛 ∈ ℂ → ( - 𝑛 · ( 2 · π ) ) = ( ( - 𝑛 · 2 ) · π ) )
19 id ⊢ ( 𝑛 ∈ ℂ → 𝑛 ∈ ℂ )
20 19 15 mulneg1d ⊢ ( 𝑛 ∈ ℂ → ( - 𝑛 · 2 ) = - ( 𝑛 · 2 ) )
21 20 oveq1d ⊢ ( 𝑛 ∈ ℂ → ( ( - 𝑛 · 2 ) · π ) = ( - ( 𝑛 · 2 ) · π ) )
22 14 18 21 3eqtrd ⊢ ( 𝑛 ∈ ℂ → ( 0 + ( - 𝑛 · ( 2 · π ) ) ) = ( - ( 𝑛 · 2 ) · π ) )
23 7 22 syl ⊢ ( 𝑛 ∈ ℤ → ( 0 + ( - 𝑛 · ( 2 · π ) ) ) = ( - ( 𝑛 · 2 ) · π ) )
24 23 adantr ⊢ ( ( 𝑛 ∈ ℤ ∧ ( 𝑛 · 2 ) = 𝐾 ) → ( 0 + ( - 𝑛 · ( 2 · π ) ) ) = ( - ( 𝑛 · 2 ) · π ) )
25 19 15 mulcld ⊢ ( 𝑛 ∈ ℂ → ( 𝑛 · 2 ) ∈ ℂ )
26 mulneg12 ⊢ ( ( ( 𝑛 · 2 ) ∈ ℂ ∧ π ∈ ℂ ) → ( - ( 𝑛 · 2 ) · π ) = ( ( 𝑛 · 2 ) · - π ) )
27 25 16 26 syl2anc ⊢ ( 𝑛 ∈ ℂ → ( - ( 𝑛 · 2 ) · π ) = ( ( 𝑛 · 2 ) · - π ) )
28 7 27 syl ⊢ ( 𝑛 ∈ ℤ → ( - ( 𝑛 · 2 ) · π ) = ( ( 𝑛 · 2 ) · - π ) )
29 28 adantr ⊢ ( ( 𝑛 ∈ ℤ ∧ ( 𝑛 · 2 ) = 𝐾 ) → ( - ( 𝑛 · 2 ) · π ) = ( ( 𝑛 · 2 ) · - π ) )
30 oveq1 ⊢ ( ( 𝑛 · 2 ) = 𝐾 → ( ( 𝑛 · 2 ) · - π ) = ( 𝐾 · - π ) )
31 30 adantl ⊢ ( ( 𝑛 ∈ ℤ ∧ ( 𝑛 · 2 ) = 𝐾 ) → ( ( 𝑛 · 2 ) · - π ) = ( 𝐾 · - π ) )
32 24 29 31 3eqtrrd ⊢ ( ( 𝑛 ∈ ℤ ∧ ( 𝑛 · 2 ) = 𝐾 ) → ( 𝐾 · - π ) = ( 0 + ( - 𝑛 · ( 2 · π ) ) ) )
33 32 fveq2d ⊢ ( ( 𝑛 ∈ ℤ ∧ ( 𝑛 · 2 ) = 𝐾 ) → ( cos ‘ ( 𝐾 · - π ) ) = ( cos ‘ ( 0 + ( - 𝑛 · ( 2 · π ) ) ) ) )
34 33 3adant1 ⊢ ( ( 2 ∥ 𝐾 ∧ 𝑛 ∈ ℤ ∧ ( 𝑛 · 2 ) = 𝐾 ) → ( cos ‘ ( 𝐾 · - π ) ) = ( cos ‘ ( 0 + ( - 𝑛 · ( 2 · π ) ) ) ) )
35 0cnd ⊢ ( 𝑛 ∈ ℤ → 0 ∈ ℂ )
36 znegcl ⊢ ( 𝑛 ∈ ℤ → - 𝑛 ∈ ℤ )
37 cosper ⊢ ( ( 0 ∈ ℂ ∧ - 𝑛 ∈ ℤ ) → ( cos ‘ ( 0 + ( - 𝑛 · ( 2 · π ) ) ) ) = ( cos ‘ 0 ) )
38 35 36 37 syl2anc ⊢ ( 𝑛 ∈ ℤ → ( cos ‘ ( 0 + ( - 𝑛 · ( 2 · π ) ) ) ) = ( cos ‘ 0 ) )
39 38 3ad2ant2 ⊢ ( ( 2 ∥ 𝐾 ∧ 𝑛 ∈ ℤ ∧ ( 𝑛 · 2 ) = 𝐾 ) → ( cos ‘ ( 0 + ( - 𝑛 · ( 2 · π ) ) ) ) = ( cos ‘ 0 ) )
40 cos0 ⊢ ( cos ‘ 0 ) = 1
41 iftrue ⊢ ( 2 ∥ 𝐾 → if ( 2 ∥ 𝐾 , 1 , - 1 ) = 1 )
42 40 41 eqtr4id ⊢ ( 2 ∥ 𝐾 → ( cos ‘ 0 ) = if ( 2 ∥ 𝐾 , 1 , - 1 ) )
43 42 3ad2ant1 ⊢ ( ( 2 ∥ 𝐾 ∧ 𝑛 ∈ ℤ ∧ ( 𝑛 · 2 ) = 𝐾 ) → ( cos ‘ 0 ) = if ( 2 ∥ 𝐾 , 1 , - 1 ) )
44 34 39 43 3eqtrd ⊢ ( ( 2 ∥ 𝐾 ∧ 𝑛 ∈ ℤ ∧ ( 𝑛 · 2 ) = 𝐾 ) → ( cos ‘ ( 𝐾 · - π ) ) = if ( 2 ∥ 𝐾 , 1 , - 1 ) )
45 44 3exp ⊢ ( 2 ∥ 𝐾 → ( 𝑛 ∈ ℤ → ( ( 𝑛 · 2 ) = 𝐾 → ( cos ‘ ( 𝐾 · - π ) ) = if ( 2 ∥ 𝐾 , 1 , - 1 ) ) ) )
46 45 adantl ⊢ ( ( 𝐾 ∈ ℤ ∧ 2 ∥ 𝐾 ) → ( 𝑛 ∈ ℤ → ( ( 𝑛 · 2 ) = 𝐾 → ( cos ‘ ( 𝐾 · - π ) ) = if ( 2 ∥ 𝐾 , 1 , - 1 ) ) ) )
47 46 rexlimdv ⊢ ( ( 𝐾 ∈ ℤ ∧ 2 ∥ 𝐾 ) → ( ∃ 𝑛 ∈ ℤ ( 𝑛 · 2 ) = 𝐾 → ( cos ‘ ( 𝐾 · - π ) ) = if ( 2 ∥ 𝐾 , 1 , - 1 ) ) )
48 6 47 mpd ⊢ ( ( 𝐾 ∈ ℤ ∧ 2 ∥ 𝐾 ) → ( cos ‘ ( 𝐾 · - π ) ) = if ( 2 ∥ 𝐾 , 1 , - 1 ) )
49 odd2np1 ⊢ ( 𝐾 ∈ ℤ → ( ¬ 2 ∥ 𝐾 ↔ ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝐾 ) )
50 49 biimpa ⊢ ( ( 𝐾 ∈ ℤ ∧ ¬ 2 ∥ 𝐾 ) → ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝐾 )
51 oveq1 ⊢ ( ( ( 2 · 𝑛 ) + 1 ) = 𝐾 → ( ( ( 2 · 𝑛 ) + 1 ) · - π ) = ( 𝐾 · - π ) )
52 51 eqcomd ⊢ ( ( ( 2 · 𝑛 ) + 1 ) = 𝐾 → ( 𝐾 · - π ) = ( ( ( 2 · 𝑛 ) + 1 ) · - π ) )
53 52 adantl ⊢ ( ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝐾 ) → ( 𝐾 · - π ) = ( ( ( 2 · 𝑛 ) + 1 ) · - π ) )
54 15 19 mulcld ⊢ ( 𝑛 ∈ ℂ → ( 2 · 𝑛 ) ∈ ℂ )
55 1cnd ⊢ ( 𝑛 ∈ ℂ → 1 ∈ ℂ )
56 negpicn ⊢ - π ∈ ℂ
57 56 a1i ⊢ ( 𝑛 ∈ ℂ → - π ∈ ℂ )
58 54 55 57 adddird ⊢ ( 𝑛 ∈ ℂ → ( ( ( 2 · 𝑛 ) + 1 ) · - π ) = ( ( ( 2 · 𝑛 ) · - π ) + ( 1 · - π ) ) )
59 7 58 syl ⊢ ( 𝑛 ∈ ℤ → ( ( ( 2 · 𝑛 ) + 1 ) · - π ) = ( ( ( 2 · 𝑛 ) · - π ) + ( 1 · - π ) ) )
60 59 adantr ⊢ ( ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝐾 ) → ( ( ( 2 · 𝑛 ) + 1 ) · - π ) = ( ( ( 2 · 𝑛 ) · - π ) + ( 1 · - π ) ) )
61 mulneg12 ⊢ ( ( ( 2 · 𝑛 ) ∈ ℂ ∧ π ∈ ℂ ) → ( - ( 2 · 𝑛 ) · π ) = ( ( 2 · 𝑛 ) · - π ) )
62 54 16 61 syl2anc ⊢ ( 𝑛 ∈ ℂ → ( - ( 2 · 𝑛 ) · π ) = ( ( 2 · 𝑛 ) · - π ) )
63 62 eqcomd ⊢ ( 𝑛 ∈ ℂ → ( ( 2 · 𝑛 ) · - π ) = ( - ( 2 · 𝑛 ) · π ) )
64 15 19 mulneg2d ⊢ ( 𝑛 ∈ ℂ → ( 2 · - 𝑛 ) = - ( 2 · 𝑛 ) )
65 15 8 mulcomd ⊢ ( 𝑛 ∈ ℂ → ( 2 · - 𝑛 ) = ( - 𝑛 · 2 ) )
66 64 65 eqtr3d ⊢ ( 𝑛 ∈ ℂ → - ( 2 · 𝑛 ) = ( - 𝑛 · 2 ) )
67 66 oveq1d ⊢ ( 𝑛 ∈ ℂ → ( - ( 2 · 𝑛 ) · π ) = ( ( - 𝑛 · 2 ) · π ) )
68 63 67 17 3eqtrd ⊢ ( 𝑛 ∈ ℂ → ( ( 2 · 𝑛 ) · - π ) = ( - 𝑛 · ( 2 · π ) ) )
69 57 mulid2d ⊢ ( 𝑛 ∈ ℂ → ( 1 · - π ) = - π )
70 68 69 oveq12d ⊢ ( 𝑛 ∈ ℂ → ( ( ( 2 · 𝑛 ) · - π ) + ( 1 · - π ) ) = ( ( - 𝑛 · ( 2 · π ) ) + - π ) )
71 13 57 addcomd ⊢ ( 𝑛 ∈ ℂ → ( ( - 𝑛 · ( 2 · π ) ) + - π ) = ( - π + ( - 𝑛 · ( 2 · π ) ) ) )
72 70 71 eqtrd ⊢ ( 𝑛 ∈ ℂ → ( ( ( 2 · 𝑛 ) · - π ) + ( 1 · - π ) ) = ( - π + ( - 𝑛 · ( 2 · π ) ) ) )
73 7 72 syl ⊢ ( 𝑛 ∈ ℤ → ( ( ( 2 · 𝑛 ) · - π ) + ( 1 · - π ) ) = ( - π + ( - 𝑛 · ( 2 · π ) ) ) )
74 73 adantr ⊢ ( ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝐾 ) → ( ( ( 2 · 𝑛 ) · - π ) + ( 1 · - π ) ) = ( - π + ( - 𝑛 · ( 2 · π ) ) ) )
75 53 60 74 3eqtrd ⊢ ( ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝐾 ) → ( 𝐾 · - π ) = ( - π + ( - 𝑛 · ( 2 · π ) ) ) )
76 75 3adant1 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝐾 ) → ( 𝐾 · - π ) = ( - π + ( - 𝑛 · ( 2 · π ) ) ) )
77 76 fveq2d ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝐾 ) → ( cos ‘ ( 𝐾 · - π ) ) = ( cos ‘ ( - π + ( - 𝑛 · ( 2 · π ) ) ) ) )
78 77 3adant1r ⊢ ( ( ( 𝐾 ∈ ℤ ∧ ¬ 2 ∥ 𝐾 ) ∧ 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝐾 ) → ( cos ‘ ( 𝐾 · - π ) ) = ( cos ‘ ( - π + ( - 𝑛 · ( 2 · π ) ) ) ) )
79 cosper ⊢ ( ( - π ∈ ℂ ∧ - 𝑛 ∈ ℤ ) → ( cos ‘ ( - π + ( - 𝑛 · ( 2 · π ) ) ) ) = ( cos ‘ - π ) )
80 56 36 79 sylancr ⊢ ( 𝑛 ∈ ℤ → ( cos ‘ ( - π + ( - 𝑛 · ( 2 · π ) ) ) ) = ( cos ‘ - π ) )
81 80 3ad2ant2 ⊢ ( ( ( 𝐾 ∈ ℤ ∧ ¬ 2 ∥ 𝐾 ) ∧ 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝐾 ) → ( cos ‘ ( - π + ( - 𝑛 · ( 2 · π ) ) ) ) = ( cos ‘ - π ) )
82 cosnegpi ⊢ ( cos ‘ - π ) = - 1
83 iffalse ⊢ ( ¬ 2 ∥ 𝐾 → if ( 2 ∥ 𝐾 , 1 , - 1 ) = - 1 )
84 82 83 eqtr4id ⊢ ( ¬ 2 ∥ 𝐾 → ( cos ‘ - π ) = if ( 2 ∥ 𝐾 , 1 , - 1 ) )
85 84 adantl ⊢ ( ( 𝐾 ∈ ℤ ∧ ¬ 2 ∥ 𝐾 ) → ( cos ‘ - π ) = if ( 2 ∥ 𝐾 , 1 , - 1 ) )
86 85 3ad2ant1 ⊢ ( ( ( 𝐾 ∈ ℤ ∧ ¬ 2 ∥ 𝐾 ) ∧ 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝐾 ) → ( cos ‘ - π ) = if ( 2 ∥ 𝐾 , 1 , - 1 ) )
87 78 81 86 3eqtrd ⊢ ( ( ( 𝐾 ∈ ℤ ∧ ¬ 2 ∥ 𝐾 ) ∧ 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝐾 ) → ( cos ‘ ( 𝐾 · - π ) ) = if ( 2 ∥ 𝐾 , 1 , - 1 ) )
88 87 rexlimdv3a ⊢ ( ( 𝐾 ∈ ℤ ∧ ¬ 2 ∥ 𝐾 ) → ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝐾 → ( cos ‘ ( 𝐾 · - π ) ) = if ( 2 ∥ 𝐾 , 1 , - 1 ) ) )
89 50 88 mpd ⊢ ( ( 𝐾 ∈ ℤ ∧ ¬ 2 ∥ 𝐾 ) → ( cos ‘ ( 𝐾 · - π ) ) = if ( 2 ∥ 𝐾 , 1 , - 1 ) )
90 48 89 pm2.61dan ⊢ ( 𝐾 ∈ ℤ → ( cos ‘ ( 𝐾 · - π ) ) = if ( 2 ∥ 𝐾 , 1 , - 1 ) )