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⁢−π=if2∥K1−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 addlidd ⊢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→if2∥K1−1=1
42 40 41 eqtr4id ⊢2∥K→cos⁡0=if2∥K1−1
43 42 3ad2ant1 ⊢2∥K∧n∈ℤ∧n⋅2=K→cos⁡0=if2∥K1−1
44 34 39 43 3eqtrd ⊢2∥K∧n∈ℤ∧n⋅2=K→cos⁡K⁢−π=if2∥K1−1
45 44 3exp ⊢2∥K→n∈ℤ→n⋅2=K→cos⁡K⁢−π=if2∥K1−1
46 45 adantl ⊢K∈ℤ∧2∥K→n∈ℤ→n⋅2=K→cos⁡K⁢−π=if2∥K1−1
47 46 rexlimdv ⊢K∈ℤ∧2∥K→∃n∈ℤn⋅2=K→cos⁡K⁢−π=if2∥K1−1
48 6 47 mpd ⊢K∈ℤ∧2∥K→cos⁡K⁢−π=if2∥K1−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 mullidd ⊢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→if2∥K1−1=−1
84 82 83 eqtr4id ⊢¬2∥K→cos⁡−π=if2∥K1−1
85 84 adantl ⊢K∈ℤ∧¬2∥K→cos⁡−π=if2∥K1−1
86 85 3ad2ant1 ⊢K∈ℤ∧¬2∥K∧n∈ℤ∧2⁢n+1=K→cos⁡−π=if2∥K1−1
87 78 81 86 3eqtrd ⊢K∈ℤ∧¬2∥K∧n∈ℤ∧2⁢n+1=K→cos⁡K⁢−π=if2∥K1−1
88 87 rexlimdv3a ⊢K∈ℤ∧¬2∥K→∃n∈ℤ2⁢n+1=K→cos⁡K⁢−π=if2∥K1−1
89 50 88 mpd ⊢K∈ℤ∧¬2∥K→cos⁡K⁢−π=if2∥K1−1
90 48 89 pm2.61dan ⊢K∈ℤ→cos⁡K⁢−π=if2∥K1−1