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 ⁢ π = if 2 ∥ K 1 − 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 → if 2 ∥ K 1 − 1 = 1
21 20 eqcomd ⊢ 2 ∥ K → 1 = if 2 ∥ K 1 − 1
22 21 3ad2ant1 ⊢ 2 ∥ K ∧ n ∈ ℤ ∧ n ⋅ 2 = K → 1 = if 2 ∥ K 1 − 1
23 19 22 eqtrd ⊢ 2 ∥ K ∧ n ∈ ℤ ∧ n ⋅ 2 = K → cos ⁡ K ⁢ π = if 2 ∥ K 1 − 1
24 23 3exp ⊢ 2 ∥ K → n ∈ ℤ → n ⋅ 2 = K → cos ⁡ K ⁢ π = if 2 ∥ K 1 − 1
25 24 adantl ⊢ K ∈ ℤ ∧ 2 ∥ K → n ∈ ℤ → n ⋅ 2 = K → cos ⁡ K ⁢ π = if 2 ∥ K 1 − 1
26 25 rexlimdv ⊢ K ∈ ℤ ∧ 2 ∥ K → ∃ n ∈ ℤ n ⋅ 2 = K → cos ⁡ K ⁢ π = if 2 ∥ K 1 − 1
27 4 26 mpd ⊢ K ∈ ℤ ∧ 2 ∥ K → cos ⁡ K ⁢ π = if 2 ∥ K 1 − 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 mulid2i ⊢ 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 → if 2 ∥ K 1 − 1 = − 1
58 57 eqcomd ⊢ ¬ 2 ∥ K → − 1 = if 2 ∥ K 1 − 1
59 58 3ad2ant1 ⊢ ¬ 2 ∥ K ∧ n ∈ ℤ ∧ 2 ⁢ n + 1 = K → − 1 = if 2 ∥ K 1 − 1
60 56 59 eqtrd ⊢ ¬ 2 ∥ K ∧ n ∈ ℤ ∧ 2 ⁢ n + 1 = K → cos ⁡ K ⁢ π = if 2 ∥ K 1 − 1
61 60 3exp ⊢ ¬ 2 ∥ K → n ∈ ℤ → 2 ⁢ n + 1 = K → cos ⁡ K ⁢ π = if 2 ∥ K 1 − 1
62 61 adantl ⊢ K ∈ ℤ ∧ ¬ 2 ∥ K → n ∈ ℤ → 2 ⁢ n + 1 = K → cos ⁡ K ⁢ π = if 2 ∥ K 1 − 1
63 62 rexlimdv ⊢ K ∈ ℤ ∧ ¬ 2 ∥ K → ∃ n ∈ ℤ 2 ⁢ n + 1 = K → cos ⁡ K ⁢ π = if 2 ∥ K 1 − 1
64 29 63 mpd ⊢ K ∈ ℤ ∧ ¬ 2 ∥ K → cos ⁡ K ⁢ π = if 2 ∥ K 1 − 1
65 27 64 pm2.61dan ⊢ K ∈ ℤ → cos ⁡ K ⁢ π = if 2 ∥ K 1 − 1