Step | Hyp | Ref
| Expression |
1 | | simpr 488 |
. . . 4
⊢ ((𝐾 ∈ ℤ ∧ 2 ∥
𝐾) → 2 ∥ 𝐾) |
2 | | 2z 12209 |
. . . . 5
⊢ 2 ∈
ℤ |
3 | | simpl 486 |
. . . . 5
⊢ ((𝐾 ∈ ℤ ∧ 2 ∥
𝐾) → 𝐾 ∈ ℤ) |
4 | | divides 15817 |
. . . . 5
⊢ ((2
∈ ℤ ∧ 𝐾
∈ ℤ) → (2 ∥ 𝐾 ↔ ∃𝑛 ∈ ℤ (𝑛 · 2) = 𝐾)) |
5 | 2, 3, 4 | sylancr 590 |
. . . 4
⊢ ((𝐾 ∈ ℤ ∧ 2 ∥
𝐾) → (2 ∥ 𝐾 ↔ ∃𝑛 ∈ ℤ (𝑛 · 2) = 𝐾)) |
6 | 1, 5 | mpbid 235 |
. . 3
⊢ ((𝐾 ∈ ℤ ∧ 2 ∥
𝐾) → ∃𝑛 ∈ ℤ (𝑛 · 2) = 𝐾) |
7 | | zcn 12181 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℂ) |
8 | | negcl 11078 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℂ → -𝑛 ∈
ℂ) |
9 | | 2cn 11905 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℂ |
10 | | picn 25349 |
. . . . . . . . . . . . . . . . 17
⊢ π
∈ ℂ |
11 | 9, 10 | mulcli 10840 |
. . . . . . . . . . . . . . . 16
⊢ (2
· π) ∈ ℂ |
12 | 11 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℂ → (2
· π) ∈ ℂ) |
13 | 8, 12 | mulcld 10853 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℂ → (-𝑛 · (2 · π))
∈ ℂ) |
14 | 13 | addid2d 11033 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℂ → (0 +
(-𝑛 · (2 ·
π))) = (-𝑛 · (2
· π))) |
15 | | 2cnd 11908 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℂ → 2 ∈
ℂ) |
16 | 10 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℂ → π
∈ ℂ) |
17 | 8, 15, 16 | mulassd 10856 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℂ → ((-𝑛 · 2) · π) =
(-𝑛 · (2 ·
π))) |
18 | 17 | eqcomd 2743 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℂ → (-𝑛 · (2 · π)) =
((-𝑛 · 2) ·
π)) |
19 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℂ → 𝑛 ∈
ℂ) |
20 | 19, 15 | mulneg1d 11285 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℂ → (-𝑛 · 2) = -(𝑛 · 2)) |
21 | 20 | oveq1d 7228 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℂ → ((-𝑛 · 2) · π) =
(-(𝑛 · 2) ·
π)) |
22 | 14, 18, 21 | 3eqtrd 2781 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℂ → (0 +
(-𝑛 · (2 ·
π))) = (-(𝑛 · 2)
· π)) |
23 | 7, 22 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℤ → (0 +
(-𝑛 · (2 ·
π))) = (-(𝑛 · 2)
· π)) |
24 | 23 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℤ ∧ (𝑛 · 2) = 𝐾) → (0 + (-𝑛 · (2 · π))) = (-(𝑛 · 2) ·
π)) |
25 | 19, 15 | mulcld 10853 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℂ → (𝑛 · 2) ∈
ℂ) |
26 | | mulneg12 11270 |
. . . . . . . . . . . . 13
⊢ (((𝑛 · 2) ∈ ℂ
∧ π ∈ ℂ) → (-(𝑛 · 2) · π) = ((𝑛 · 2) ·
-π)) |
27 | 25, 16, 26 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℂ → (-(𝑛 · 2) · π) =
((𝑛 · 2) ·
-π)) |
28 | 7, 27 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℤ → (-(𝑛 · 2) · π) =
((𝑛 · 2) ·
-π)) |
29 | 28 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℤ ∧ (𝑛 · 2) = 𝐾) → (-(𝑛 · 2) · π) = ((𝑛 · 2) ·
-π)) |
30 | | oveq1 7220 |
. . . . . . . . . . 11
⊢ ((𝑛 · 2) = 𝐾 → ((𝑛 · 2) · -π) = (𝐾 ·
-π)) |
31 | 30 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℤ ∧ (𝑛 · 2) = 𝐾) → ((𝑛 · 2) · -π) = (𝐾 ·
-π)) |
32 | 24, 29, 31 | 3eqtrrd 2782 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ (𝑛 · 2) = 𝐾) → (𝐾 · -π) = (0 + (-𝑛 · (2 ·
π)))) |
33 | 32 | fveq2d 6721 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℤ ∧ (𝑛 · 2) = 𝐾) → (cos‘(𝐾 · -π)) = (cos‘(0 + (-𝑛 · (2 ·
π))))) |
34 | 33 | 3adant1 1132 |
. . . . . . 7
⊢ ((2
∥ 𝐾 ∧ 𝑛 ∈ ℤ ∧ (𝑛 · 2) = 𝐾) → (cos‘(𝐾 · -π)) = (cos‘(0 + (-𝑛 · (2 ·
π))))) |
35 | | 0cnd 10826 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℤ → 0 ∈
ℂ) |
36 | | znegcl 12212 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℤ → -𝑛 ∈
ℤ) |
37 | | cosper 25372 |
. . . . . . . . 9
⊢ ((0
∈ ℂ ∧ -𝑛
∈ ℤ) → (cos‘(0 + (-𝑛 · (2 · π)))) =
(cos‘0)) |
38 | 35, 36, 37 | syl2anc 587 |
. . . . . . . 8
⊢ (𝑛 ∈ ℤ →
(cos‘(0 + (-𝑛
· (2 · π)))) = (cos‘0)) |
39 | 38 | 3ad2ant2 1136 |
. . . . . . 7
⊢ ((2
∥ 𝐾 ∧ 𝑛 ∈ ℤ ∧ (𝑛 · 2) = 𝐾) → (cos‘(0 + (-𝑛 · (2 · π)))) =
(cos‘0)) |
40 | | cos0 15711 |
. . . . . . . . 9
⊢
(cos‘0) = 1 |
41 | | iftrue 4445 |
. . . . . . . . 9
⊢ (2
∥ 𝐾 → if(2
∥ 𝐾, 1, -1) =
1) |
42 | 40, 41 | eqtr4id 2797 |
. . . . . . . 8
⊢ (2
∥ 𝐾 →
(cos‘0) = if(2 ∥ 𝐾, 1, -1)) |
43 | 42 | 3ad2ant1 1135 |
. . . . . . 7
⊢ ((2
∥ 𝐾 ∧ 𝑛 ∈ ℤ ∧ (𝑛 · 2) = 𝐾) → (cos‘0) = if(2 ∥ 𝐾, 1, -1)) |
44 | 34, 39, 43 | 3eqtrd 2781 |
. . . . . 6
⊢ ((2
∥ 𝐾 ∧ 𝑛 ∈ ℤ ∧ (𝑛 · 2) = 𝐾) → (cos‘(𝐾 · -π)) = if(2 ∥ 𝐾, 1, -1)) |
45 | 44 | 3exp 1121 |
. . . . 5
⊢ (2
∥ 𝐾 → (𝑛 ∈ ℤ → ((𝑛 · 2) = 𝐾 → (cos‘(𝐾 · -π)) = if(2 ∥ 𝐾, 1, -1)))) |
46 | 45 | adantl 485 |
. . . 4
⊢ ((𝐾 ∈ ℤ ∧ 2 ∥
𝐾) → (𝑛 ∈ ℤ → ((𝑛 · 2) = 𝐾 → (cos‘(𝐾 · -π)) = if(2 ∥ 𝐾, 1, -1)))) |
47 | 46 | rexlimdv 3202 |
. . 3
⊢ ((𝐾 ∈ ℤ ∧ 2 ∥
𝐾) → (∃𝑛 ∈ ℤ (𝑛 · 2) = 𝐾 → (cos‘(𝐾 · -π)) = if(2 ∥ 𝐾, 1, -1))) |
48 | 6, 47 | mpd 15 |
. 2
⊢ ((𝐾 ∈ ℤ ∧ 2 ∥
𝐾) → (cos‘(𝐾 · -π)) = if(2 ∥
𝐾, 1, -1)) |
49 | | odd2np1 15902 |
. . . 4
⊢ (𝐾 ∈ ℤ → (¬ 2
∥ 𝐾 ↔
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝐾)) |
50 | 49 | biimpa 480 |
. . 3
⊢ ((𝐾 ∈ ℤ ∧ ¬ 2
∥ 𝐾) →
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝐾) |
51 | | oveq1 7220 |
. . . . . . . . . . 11
⊢ (((2
· 𝑛) + 1) = 𝐾 → (((2 · 𝑛) + 1) · -π) = (𝐾 ·
-π)) |
52 | 51 | eqcomd 2743 |
. . . . . . . . . 10
⊢ (((2
· 𝑛) + 1) = 𝐾 → (𝐾 · -π) = (((2 · 𝑛) + 1) ·
-π)) |
53 | 52 | adantl 485 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝐾) → (𝐾 · -π) = (((2 · 𝑛) + 1) ·
-π)) |
54 | 15, 19 | mulcld 10853 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℂ → (2
· 𝑛) ∈
ℂ) |
55 | | 1cnd 10828 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℂ → 1 ∈
ℂ) |
56 | | negpicn 25352 |
. . . . . . . . . . . . 13
⊢ -π
∈ ℂ |
57 | 56 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℂ → -π
∈ ℂ) |
58 | 54, 55, 57 | adddird 10858 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℂ → (((2
· 𝑛) + 1) ·
-π) = (((2 · 𝑛)
· -π) + (1 · -π))) |
59 | 7, 58 | syl 17 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℤ → (((2
· 𝑛) + 1) ·
-π) = (((2 · 𝑛)
· -π) + (1 · -π))) |
60 | 59 | adantr 484 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝐾) → (((2 · 𝑛) + 1) · -π) = (((2
· 𝑛) · -π)
+ (1 · -π))) |
61 | | mulneg12 11270 |
. . . . . . . . . . . . . . . 16
⊢ (((2
· 𝑛) ∈ ℂ
∧ π ∈ ℂ) → (-(2 · 𝑛) · π) = ((2 · 𝑛) ·
-π)) |
62 | 54, 16, 61 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℂ → (-(2
· 𝑛) · π)
= ((2 · 𝑛) ·
-π)) |
63 | 62 | eqcomd 2743 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℂ → ((2
· 𝑛) · -π)
= (-(2 · 𝑛) ·
π)) |
64 | 15, 19 | mulneg2d 11286 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℂ → (2
· -𝑛) = -(2 ·
𝑛)) |
65 | 15, 8 | mulcomd 10854 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℂ → (2
· -𝑛) = (-𝑛 · 2)) |
66 | 64, 65 | eqtr3d 2779 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℂ → -(2
· 𝑛) = (-𝑛 · 2)) |
67 | 66 | oveq1d 7228 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℂ → (-(2
· 𝑛) · π)
= ((-𝑛 · 2) ·
π)) |
68 | 63, 67, 17 | 3eqtrd 2781 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℂ → ((2
· 𝑛) · -π)
= (-𝑛 · (2 ·
π))) |
69 | 57 | mulid2d 10851 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℂ → (1
· -π) = -π) |
70 | 68, 69 | oveq12d 7231 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℂ → (((2
· 𝑛) · -π)
+ (1 · -π)) = ((-𝑛 · (2 · π)) +
-π)) |
71 | 13, 57 | addcomd 11034 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℂ → ((-𝑛 · (2 · π)) +
-π) = (-π + (-𝑛
· (2 · π)))) |
72 | 70, 71 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℂ → (((2
· 𝑛) · -π)
+ (1 · -π)) = (-π + (-𝑛 · (2 ·
π)))) |
73 | 7, 72 | syl 17 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℤ → (((2
· 𝑛) · -π)
+ (1 · -π)) = (-π + (-𝑛 · (2 ·
π)))) |
74 | 73 | adantr 484 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝐾) → (((2 · 𝑛) · -π) + (1 ·
-π)) = (-π + (-𝑛
· (2 · π)))) |
75 | 53, 60, 74 | 3eqtrd 2781 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝐾) → (𝐾 · -π) = (-π + (-𝑛 · (2 ·
π)))) |
76 | 75 | 3adant1 1132 |
. . . . . . 7
⊢ ((𝐾 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝐾) → (𝐾 · -π) = (-π + (-𝑛 · (2 ·
π)))) |
77 | 76 | fveq2d 6721 |
. . . . . 6
⊢ ((𝐾 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝐾) → (cos‘(𝐾 · -π)) =
(cos‘(-π + (-𝑛
· (2 · π))))) |
78 | 77 | 3adant1r 1179 |
. . . . 5
⊢ (((𝐾 ∈ ℤ ∧ ¬ 2
∥ 𝐾) ∧ 𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝐾) → (cos‘(𝐾 · -π)) =
(cos‘(-π + (-𝑛
· (2 · π))))) |
79 | | cosper 25372 |
. . . . . . 7
⊢ ((-π
∈ ℂ ∧ -𝑛
∈ ℤ) → (cos‘(-π + (-𝑛 · (2 · π)))) =
(cos‘-π)) |
80 | 56, 36, 79 | sylancr 590 |
. . . . . 6
⊢ (𝑛 ∈ ℤ →
(cos‘(-π + (-𝑛
· (2 · π)))) = (cos‘-π)) |
81 | 80 | 3ad2ant2 1136 |
. . . . 5
⊢ (((𝐾 ∈ ℤ ∧ ¬ 2
∥ 𝐾) ∧ 𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝐾) → (cos‘(-π +
(-𝑛 · (2 ·
π)))) = (cos‘-π)) |
82 | | cosnegpi 43083 |
. . . . . . . 8
⊢
(cos‘-π) = -1 |
83 | | iffalse 4448 |
. . . . . . . 8
⊢ (¬ 2
∥ 𝐾 → if(2
∥ 𝐾, 1, -1) =
-1) |
84 | 82, 83 | eqtr4id 2797 |
. . . . . . 7
⊢ (¬ 2
∥ 𝐾 →
(cos‘-π) = if(2 ∥ 𝐾, 1, -1)) |
85 | 84 | adantl 485 |
. . . . . 6
⊢ ((𝐾 ∈ ℤ ∧ ¬ 2
∥ 𝐾) →
(cos‘-π) = if(2 ∥ 𝐾, 1, -1)) |
86 | 85 | 3ad2ant1 1135 |
. . . . 5
⊢ (((𝐾 ∈ ℤ ∧ ¬ 2
∥ 𝐾) ∧ 𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝐾) → (cos‘-π) =
if(2 ∥ 𝐾, 1,
-1)) |
87 | 78, 81, 86 | 3eqtrd 2781 |
. . . 4
⊢ (((𝐾 ∈ ℤ ∧ ¬ 2
∥ 𝐾) ∧ 𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝐾) → (cos‘(𝐾 · -π)) = if(2 ∥
𝐾, 1, -1)) |
88 | 87 | rexlimdv3a 3205 |
. . 3
⊢ ((𝐾 ∈ ℤ ∧ ¬ 2
∥ 𝐾) →
(∃𝑛 ∈ ℤ
((2 · 𝑛) + 1) =
𝐾 → (cos‘(𝐾 · -π)) = if(2 ∥
𝐾, 1,
-1))) |
89 | 50, 88 | mpd 15 |
. 2
⊢ ((𝐾 ∈ ℤ ∧ ¬ 2
∥ 𝐾) →
(cos‘(𝐾 ·
-π)) = if(2 ∥ 𝐾,
1, -1)) |
90 | 48, 89 | pm2.61dan 813 |
1
⊢ (𝐾 ∈ ℤ →
(cos‘(𝐾 ·
-π)) = if(2 ∥ 𝐾,
1, -1)) |