Step | Hyp | Ref
| Expression |
1 | | simpr 487 |
. . . 4
⊢ ((𝐾 ∈ ℤ ∧ 2 ∥
𝐾) → 2 ∥ 𝐾) |
2 | | 2z 12015 |
. . . . 5
⊢ 2 ∈
ℤ |
3 | | simpl 485 |
. . . . 5
⊢ ((𝐾 ∈ ℤ ∧ 2 ∥
𝐾) → 𝐾 ∈ ℤ) |
4 | | divides 15609 |
. . . . 5
⊢ ((2
∈ ℤ ∧ 𝐾
∈ ℤ) → (2 ∥ 𝐾 ↔ ∃𝑛 ∈ ℤ (𝑛 · 2) = 𝐾)) |
5 | 2, 3, 4 | sylancr 589 |
. . . 4
⊢ ((𝐾 ∈ ℤ ∧ 2 ∥
𝐾) → (2 ∥ 𝐾 ↔ ∃𝑛 ∈ ℤ (𝑛 · 2) = 𝐾)) |
6 | 1, 5 | mpbid 234 |
. . 3
⊢ ((𝐾 ∈ ℤ ∧ 2 ∥
𝐾) → ∃𝑛 ∈ ℤ (𝑛 · 2) = 𝐾) |
7 | | zcn 11987 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℂ) |
8 | | negcl 10886 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℂ → -𝑛 ∈
ℂ) |
9 | | 2cn 11713 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℂ |
10 | | picn 25045 |
. . . . . . . . . . . . . . . . 17
⊢ π
∈ ℂ |
11 | 9, 10 | mulcli 10648 |
. . . . . . . . . . . . . . . 16
⊢ (2
· π) ∈ ℂ |
12 | 11 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℂ → (2
· π) ∈ ℂ) |
13 | 8, 12 | mulcld 10661 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℂ → (-𝑛 · (2 · π))
∈ ℂ) |
14 | 13 | addid2d 10841 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℂ → (0 +
(-𝑛 · (2 ·
π))) = (-𝑛 · (2
· π))) |
15 | | 2cnd 11716 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℂ → 2 ∈
ℂ) |
16 | 10 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℂ → π
∈ ℂ) |
17 | 8, 15, 16 | mulassd 10664 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℂ → ((-𝑛 · 2) · π) =
(-𝑛 · (2 ·
π))) |
18 | 17 | eqcomd 2827 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℂ → (-𝑛 · (2 · π)) =
((-𝑛 · 2) ·
π)) |
19 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℂ → 𝑛 ∈
ℂ) |
20 | 19, 15 | mulneg1d 11093 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℂ → (-𝑛 · 2) = -(𝑛 · 2)) |
21 | 20 | oveq1d 7171 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℂ → ((-𝑛 · 2) · π) =
(-(𝑛 · 2) ·
π)) |
22 | 14, 18, 21 | 3eqtrd 2860 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℂ → (0 +
(-𝑛 · (2 ·
π))) = (-(𝑛 · 2)
· π)) |
23 | 7, 22 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℤ → (0 +
(-𝑛 · (2 ·
π))) = (-(𝑛 · 2)
· π)) |
24 | 23 | adantr 483 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℤ ∧ (𝑛 · 2) = 𝐾) → (0 + (-𝑛 · (2 · π))) = (-(𝑛 · 2) ·
π)) |
25 | 19, 15 | mulcld 10661 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℂ → (𝑛 · 2) ∈
ℂ) |
26 | | mulneg12 11078 |
. . . . . . . . . . . . 13
⊢ (((𝑛 · 2) ∈ ℂ
∧ π ∈ ℂ) → (-(𝑛 · 2) · π) = ((𝑛 · 2) ·
-π)) |
27 | 25, 16, 26 | syl2anc 586 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℂ → (-(𝑛 · 2) · π) =
((𝑛 · 2) ·
-π)) |
28 | 7, 27 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℤ → (-(𝑛 · 2) · π) =
((𝑛 · 2) ·
-π)) |
29 | 28 | adantr 483 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℤ ∧ (𝑛 · 2) = 𝐾) → (-(𝑛 · 2) · π) = ((𝑛 · 2) ·
-π)) |
30 | | oveq1 7163 |
. . . . . . . . . . 11
⊢ ((𝑛 · 2) = 𝐾 → ((𝑛 · 2) · -π) = (𝐾 ·
-π)) |
31 | 30 | adantl 484 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℤ ∧ (𝑛 · 2) = 𝐾) → ((𝑛 · 2) · -π) = (𝐾 ·
-π)) |
32 | 24, 29, 31 | 3eqtrrd 2861 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ (𝑛 · 2) = 𝐾) → (𝐾 · -π) = (0 + (-𝑛 · (2 ·
π)))) |
33 | 32 | fveq2d 6674 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℤ ∧ (𝑛 · 2) = 𝐾) → (cos‘(𝐾 · -π)) = (cos‘(0 + (-𝑛 · (2 ·
π))))) |
34 | 33 | 3adant1 1126 |
. . . . . . 7
⊢ ((2
∥ 𝐾 ∧ 𝑛 ∈ ℤ ∧ (𝑛 · 2) = 𝐾) → (cos‘(𝐾 · -π)) = (cos‘(0 + (-𝑛 · (2 ·
π))))) |
35 | | 0cnd 10634 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℤ → 0 ∈
ℂ) |
36 | | znegcl 12018 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℤ → -𝑛 ∈
ℤ) |
37 | | cosper 25068 |
. . . . . . . . 9
⊢ ((0
∈ ℂ ∧ -𝑛
∈ ℤ) → (cos‘(0 + (-𝑛 · (2 · π)))) =
(cos‘0)) |
38 | 35, 36, 37 | syl2anc 586 |
. . . . . . . 8
⊢ (𝑛 ∈ ℤ →
(cos‘(0 + (-𝑛
· (2 · π)))) = (cos‘0)) |
39 | 38 | 3ad2ant2 1130 |
. . . . . . 7
⊢ ((2
∥ 𝐾 ∧ 𝑛 ∈ ℤ ∧ (𝑛 · 2) = 𝐾) → (cos‘(0 + (-𝑛 · (2 · π)))) =
(cos‘0)) |
40 | | iftrue 4473 |
. . . . . . . . 9
⊢ (2
∥ 𝐾 → if(2
∥ 𝐾, 1, -1) =
1) |
41 | | cos0 15503 |
. . . . . . . . 9
⊢
(cos‘0) = 1 |
42 | 40, 41 | syl6reqr 2875 |
. . . . . . . 8
⊢ (2
∥ 𝐾 →
(cos‘0) = if(2 ∥ 𝐾, 1, -1)) |
43 | 42 | 3ad2ant1 1129 |
. . . . . . 7
⊢ ((2
∥ 𝐾 ∧ 𝑛 ∈ ℤ ∧ (𝑛 · 2) = 𝐾) → (cos‘0) = if(2 ∥ 𝐾, 1, -1)) |
44 | 34, 39, 43 | 3eqtrd 2860 |
. . . . . 6
⊢ ((2
∥ 𝐾 ∧ 𝑛 ∈ ℤ ∧ (𝑛 · 2) = 𝐾) → (cos‘(𝐾 · -π)) = if(2 ∥ 𝐾, 1, -1)) |
45 | 44 | 3exp 1115 |
. . . . 5
⊢ (2
∥ 𝐾 → (𝑛 ∈ ℤ → ((𝑛 · 2) = 𝐾 → (cos‘(𝐾 · -π)) = if(2 ∥ 𝐾, 1, -1)))) |
46 | 45 | adantl 484 |
. . . 4
⊢ ((𝐾 ∈ ℤ ∧ 2 ∥
𝐾) → (𝑛 ∈ ℤ → ((𝑛 · 2) = 𝐾 → (cos‘(𝐾 · -π)) = if(2 ∥ 𝐾, 1, -1)))) |
47 | 46 | rexlimdv 3283 |
. . 3
⊢ ((𝐾 ∈ ℤ ∧ 2 ∥
𝐾) → (∃𝑛 ∈ ℤ (𝑛 · 2) = 𝐾 → (cos‘(𝐾 · -π)) = if(2 ∥ 𝐾, 1, -1))) |
48 | 6, 47 | mpd 15 |
. 2
⊢ ((𝐾 ∈ ℤ ∧ 2 ∥
𝐾) → (cos‘(𝐾 · -π)) = if(2 ∥
𝐾, 1, -1)) |
49 | | odd2np1 15690 |
. . . 4
⊢ (𝐾 ∈ ℤ → (¬ 2
∥ 𝐾 ↔
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝐾)) |
50 | 49 | biimpa 479 |
. . 3
⊢ ((𝐾 ∈ ℤ ∧ ¬ 2
∥ 𝐾) →
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝐾) |
51 | | oveq1 7163 |
. . . . . . . . . . 11
⊢ (((2
· 𝑛) + 1) = 𝐾 → (((2 · 𝑛) + 1) · -π) = (𝐾 ·
-π)) |
52 | 51 | eqcomd 2827 |
. . . . . . . . . 10
⊢ (((2
· 𝑛) + 1) = 𝐾 → (𝐾 · -π) = (((2 · 𝑛) + 1) ·
-π)) |
53 | 52 | adantl 484 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝐾) → (𝐾 · -π) = (((2 · 𝑛) + 1) ·
-π)) |
54 | 15, 19 | mulcld 10661 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℂ → (2
· 𝑛) ∈
ℂ) |
55 | | 1cnd 10636 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℂ → 1 ∈
ℂ) |
56 | | negpicn 25048 |
. . . . . . . . . . . . 13
⊢ -π
∈ ℂ |
57 | 56 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℂ → -π
∈ ℂ) |
58 | 54, 55, 57 | adddird 10666 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℂ → (((2
· 𝑛) + 1) ·
-π) = (((2 · 𝑛)
· -π) + (1 · -π))) |
59 | 7, 58 | syl 17 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℤ → (((2
· 𝑛) + 1) ·
-π) = (((2 · 𝑛)
· -π) + (1 · -π))) |
60 | 59 | adantr 483 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝐾) → (((2 · 𝑛) + 1) · -π) = (((2
· 𝑛) · -π)
+ (1 · -π))) |
61 | | mulneg12 11078 |
. . . . . . . . . . . . . . . 16
⊢ (((2
· 𝑛) ∈ ℂ
∧ π ∈ ℂ) → (-(2 · 𝑛) · π) = ((2 · 𝑛) ·
-π)) |
62 | 54, 16, 61 | syl2anc 586 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℂ → (-(2
· 𝑛) · π)
= ((2 · 𝑛) ·
-π)) |
63 | 62 | eqcomd 2827 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℂ → ((2
· 𝑛) · -π)
= (-(2 · 𝑛) ·
π)) |
64 | 15, 19 | mulneg2d 11094 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℂ → (2
· -𝑛) = -(2 ·
𝑛)) |
65 | 15, 8 | mulcomd 10662 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℂ → (2
· -𝑛) = (-𝑛 · 2)) |
66 | 64, 65 | eqtr3d 2858 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℂ → -(2
· 𝑛) = (-𝑛 · 2)) |
67 | 66 | oveq1d 7171 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℂ → (-(2
· 𝑛) · π)
= ((-𝑛 · 2) ·
π)) |
68 | 63, 67, 17 | 3eqtrd 2860 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℂ → ((2
· 𝑛) · -π)
= (-𝑛 · (2 ·
π))) |
69 | 57 | mulid2d 10659 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℂ → (1
· -π) = -π) |
70 | 68, 69 | oveq12d 7174 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℂ → (((2
· 𝑛) · -π)
+ (1 · -π)) = ((-𝑛 · (2 · π)) +
-π)) |
71 | 13, 57 | addcomd 10842 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℂ → ((-𝑛 · (2 · π)) +
-π) = (-π + (-𝑛
· (2 · π)))) |
72 | 70, 71 | eqtrd 2856 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℂ → (((2
· 𝑛) · -π)
+ (1 · -π)) = (-π + (-𝑛 · (2 ·
π)))) |
73 | 7, 72 | syl 17 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℤ → (((2
· 𝑛) · -π)
+ (1 · -π)) = (-π + (-𝑛 · (2 ·
π)))) |
74 | 73 | adantr 483 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝐾) → (((2 · 𝑛) · -π) + (1 ·
-π)) = (-π + (-𝑛
· (2 · π)))) |
75 | 53, 60, 74 | 3eqtrd 2860 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝐾) → (𝐾 · -π) = (-π + (-𝑛 · (2 ·
π)))) |
76 | 75 | 3adant1 1126 |
. . . . . . 7
⊢ ((𝐾 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝐾) → (𝐾 · -π) = (-π + (-𝑛 · (2 ·
π)))) |
77 | 76 | fveq2d 6674 |
. . . . . 6
⊢ ((𝐾 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝐾) → (cos‘(𝐾 · -π)) =
(cos‘(-π + (-𝑛
· (2 · π))))) |
78 | 77 | 3adant1r 1173 |
. . . . 5
⊢ (((𝐾 ∈ ℤ ∧ ¬ 2
∥ 𝐾) ∧ 𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝐾) → (cos‘(𝐾 · -π)) =
(cos‘(-π + (-𝑛
· (2 · π))))) |
79 | | cosper 25068 |
. . . . . . 7
⊢ ((-π
∈ ℂ ∧ -𝑛
∈ ℤ) → (cos‘(-π + (-𝑛 · (2 · π)))) =
(cos‘-π)) |
80 | 56, 36, 79 | sylancr 589 |
. . . . . 6
⊢ (𝑛 ∈ ℤ →
(cos‘(-π + (-𝑛
· (2 · π)))) = (cos‘-π)) |
81 | 80 | 3ad2ant2 1130 |
. . . . 5
⊢ (((𝐾 ∈ ℤ ∧ ¬ 2
∥ 𝐾) ∧ 𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝐾) → (cos‘(-π +
(-𝑛 · (2 ·
π)))) = (cos‘-π)) |
82 | | iffalse 4476 |
. . . . . . . 8
⊢ (¬ 2
∥ 𝐾 → if(2
∥ 𝐾, 1, -1) =
-1) |
83 | | cosnegpi 42168 |
. . . . . . . 8
⊢
(cos‘-π) = -1 |
84 | 82, 83 | syl6reqr 2875 |
. . . . . . 7
⊢ (¬ 2
∥ 𝐾 →
(cos‘-π) = if(2 ∥ 𝐾, 1, -1)) |
85 | 84 | adantl 484 |
. . . . . 6
⊢ ((𝐾 ∈ ℤ ∧ ¬ 2
∥ 𝐾) →
(cos‘-π) = if(2 ∥ 𝐾, 1, -1)) |
86 | 85 | 3ad2ant1 1129 |
. . . . 5
⊢ (((𝐾 ∈ ℤ ∧ ¬ 2
∥ 𝐾) ∧ 𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝐾) → (cos‘-π) =
if(2 ∥ 𝐾, 1,
-1)) |
87 | 78, 81, 86 | 3eqtrd 2860 |
. . . 4
⊢ (((𝐾 ∈ ℤ ∧ ¬ 2
∥ 𝐾) ∧ 𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝐾) → (cos‘(𝐾 · -π)) = if(2 ∥
𝐾, 1, -1)) |
88 | 87 | rexlimdv3a 3286 |
. . 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 811 |
1
⊢ (𝐾 ∈ ℤ →
(cos‘(𝐾 ·
-π)) = if(2 ∥ 𝐾,
1, -1)) |