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

Proof

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