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 ⊢ K ∈ ℤ → cos ⁡ K ⁢ − π = if 2 ∥ K 1 − 1

Proof

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