Step | Hyp | Ref
| Expression |
1 | | 2z 9233 |
. . . . . . 7
⊢ 2 ∈
ℤ |
2 | | divides 11744 |
. . . . . . 7
⊢ ((2
∈ ℤ ∧ 𝑁
∈ ℤ) → (2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℤ (𝑛 · 2) = 𝑁)) |
3 | 1, 2 | mpan 422 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → (2
∥ 𝑁 ↔
∃𝑛 ∈ ℤ
(𝑛 · 2) = 𝑁)) |
4 | | oveq2 5859 |
. . . . . . . . 9
⊢ (𝑁 = (𝑛 · 2) → (-1↑𝑁) = (-1↑(𝑛 · 2))) |
5 | 4 | eqcoms 2173 |
. . . . . . . 8
⊢ ((𝑛 · 2) = 𝑁 → (-1↑𝑁) = (-1↑(𝑛 · 2))) |
6 | | zcn 9210 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℂ) |
7 | | 2cnd 8944 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℤ → 2 ∈
ℂ) |
8 | 6, 7 | mulcomd 7934 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℤ → (𝑛 · 2) = (2 · 𝑛)) |
9 | 8 | oveq2d 5867 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℤ →
(-1↑(𝑛 · 2)) =
(-1↑(2 · 𝑛))) |
10 | | m1expeven 10516 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℤ →
(-1↑(2 · 𝑛)) =
1) |
11 | 9, 10 | eqtrd 2203 |
. . . . . . . 8
⊢ (𝑛 ∈ ℤ →
(-1↑(𝑛 · 2)) =
1) |
12 | 5, 11 | sylan9eqr 2225 |
. . . . . . 7
⊢ ((𝑛 ∈ ℤ ∧ (𝑛 · 2) = 𝑁) → (-1↑𝑁) = 1) |
13 | 12 | rexlimiva 2582 |
. . . . . 6
⊢
(∃𝑛 ∈
ℤ (𝑛 · 2) =
𝑁 → (-1↑𝑁) = 1) |
14 | 3, 13 | syl6bi 162 |
. . . . 5
⊢ (𝑁 ∈ ℤ → (2
∥ 𝑁 →
(-1↑𝑁) =
1)) |
15 | 14 | impcom 124 |
. . . 4
⊢ ((2
∥ 𝑁 ∧ 𝑁 ∈ ℤ) →
(-1↑𝑁) =
1) |
16 | | simpl 108 |
. . . 4
⊢ ((2
∥ 𝑁 ∧ 𝑁 ∈ ℤ) → 2
∥ 𝑁) |
17 | 15, 16 | 2thd 174 |
. . 3
⊢ ((2
∥ 𝑁 ∧ 𝑁 ∈ ℤ) →
((-1↑𝑁) = 1 ↔ 2
∥ 𝑁)) |
18 | 17 | expcom 115 |
. 2
⊢ (𝑁 ∈ ℤ → (2
∥ 𝑁 →
((-1↑𝑁) = 1 ↔ 2
∥ 𝑁))) |
19 | | 1ne0 8939 |
. . . . . 6
⊢ 1 ≠
0 |
20 | | eqcom 2172 |
. . . . . . 7
⊢ (-1 = 1
↔ 1 = -1) |
21 | | ax-1cn 7860 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
22 | 21 | eqnegi 8651 |
. . . . . . 7
⊢ (1 = -1
↔ 1 = 0) |
23 | 20, 22 | bitri 183 |
. . . . . 6
⊢ (-1 = 1
↔ 1 = 0) |
24 | 19, 23 | nemtbir 2429 |
. . . . 5
⊢ ¬ -1
= 1 |
25 | | odd2np1 11825 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → (¬ 2
∥ 𝑁 ↔
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁)) |
26 | | oveq2 5859 |
. . . . . . . . . . 11
⊢ (𝑁 = ((2 · 𝑛) + 1) → (-1↑𝑁) = (-1↑((2 · 𝑛) + 1))) |
27 | 26 | eqcoms 2173 |
. . . . . . . . . 10
⊢ (((2
· 𝑛) + 1) = 𝑁 → (-1↑𝑁) = (-1↑((2 · 𝑛) + 1))) |
28 | | neg1cn 8976 |
. . . . . . . . . . . . 13
⊢ -1 ∈
ℂ |
29 | 28 | a1i 9 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ → -1 ∈
ℂ) |
30 | | neg1ap0 8980 |
. . . . . . . . . . . . 13
⊢ -1 #
0 |
31 | 30 | a1i 9 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ → -1 #
0) |
32 | 1 | a1i 9 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℤ → 2 ∈
ℤ) |
33 | | id 19 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℤ) |
34 | 32, 33 | zmulcld 9333 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ → (2
· 𝑛) ∈
ℤ) |
35 | 29, 31, 34 | expp1zapd 10611 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℤ →
(-1↑((2 · 𝑛) +
1)) = ((-1↑(2 · 𝑛)) · -1)) |
36 | 10 | oveq1d 5866 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ →
((-1↑(2 · 𝑛))
· -1) = (1 · -1)) |
37 | 28 | mulid2i 7916 |
. . . . . . . . . . . 12
⊢ (1
· -1) = -1 |
38 | 36, 37 | eqtrdi 2219 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℤ →
((-1↑(2 · 𝑛))
· -1) = -1) |
39 | 35, 38 | eqtrd 2203 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℤ →
(-1↑((2 · 𝑛) +
1)) = -1) |
40 | 27, 39 | sylan9eqr 2225 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝑁) → (-1↑𝑁) = -1) |
41 | 40 | rexlimiva 2582 |
. . . . . . . 8
⊢
(∃𝑛 ∈
ℤ ((2 · 𝑛) +
1) = 𝑁 →
(-1↑𝑁) =
-1) |
42 | 25, 41 | syl6bi 162 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ → (¬ 2
∥ 𝑁 →
(-1↑𝑁) =
-1)) |
43 | 42 | impcom 124 |
. . . . . 6
⊢ ((¬ 2
∥ 𝑁 ∧ 𝑁 ∈ ℤ) →
(-1↑𝑁) =
-1) |
44 | 43 | eqeq1d 2179 |
. . . . 5
⊢ ((¬ 2
∥ 𝑁 ∧ 𝑁 ∈ ℤ) →
((-1↑𝑁) = 1 ↔ -1
= 1)) |
45 | 24, 44 | mtbiri 670 |
. . . 4
⊢ ((¬ 2
∥ 𝑁 ∧ 𝑁 ∈ ℤ) → ¬
(-1↑𝑁) =
1) |
46 | | simpl 108 |
. . . 4
⊢ ((¬ 2
∥ 𝑁 ∧ 𝑁 ∈ ℤ) → ¬ 2
∥ 𝑁) |
47 | 45, 46 | 2falsed 697 |
. . 3
⊢ ((¬ 2
∥ 𝑁 ∧ 𝑁 ∈ ℤ) →
((-1↑𝑁) = 1 ↔ 2
∥ 𝑁)) |
48 | 47 | expcom 115 |
. 2
⊢ (𝑁 ∈ ℤ → (¬ 2
∥ 𝑁 →
((-1↑𝑁) = 1 ↔ 2
∥ 𝑁))) |
49 | | zeo3 11820 |
. 2
⊢ (𝑁 ∈ ℤ → (2
∥ 𝑁 ∨ ¬ 2
∥ 𝑁)) |
50 | 18, 48, 49 | mpjaod 713 |
1
⊢ (𝑁 ∈ ℤ →
((-1↑𝑁) = 1 ↔ 2
∥ 𝑁)) |