Step |
Hyp |
Ref |
Expression |
1 |
|
2z |
⊢ 2 ∈ ℤ |
2 |
|
divides |
⊢ ( ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 · 2 ) = 𝑁 ) ) |
3 |
1 2
|
mpan |
⊢ ( 𝑁 ∈ ℤ → ( 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 · 2 ) = 𝑁 ) ) |
4 |
|
oveq2 |
⊢ ( 𝑁 = ( 𝑛 · 2 ) → ( - 1 ↑ 𝑁 ) = ( - 1 ↑ ( 𝑛 · 2 ) ) ) |
5 |
4
|
eqcoms |
⊢ ( ( 𝑛 · 2 ) = 𝑁 → ( - 1 ↑ 𝑁 ) = ( - 1 ↑ ( 𝑛 · 2 ) ) ) |
6 |
|
zcn |
⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℂ ) |
7 |
|
2cnd |
⊢ ( 𝑛 ∈ ℤ → 2 ∈ ℂ ) |
8 |
6 7
|
mulcomd |
⊢ ( 𝑛 ∈ ℤ → ( 𝑛 · 2 ) = ( 2 · 𝑛 ) ) |
9 |
8
|
oveq2d |
⊢ ( 𝑛 ∈ ℤ → ( - 1 ↑ ( 𝑛 · 2 ) ) = ( - 1 ↑ ( 2 · 𝑛 ) ) ) |
10 |
|
m1expeven |
⊢ ( 𝑛 ∈ ℤ → ( - 1 ↑ ( 2 · 𝑛 ) ) = 1 ) |
11 |
9 10
|
eqtrd |
⊢ ( 𝑛 ∈ ℤ → ( - 1 ↑ ( 𝑛 · 2 ) ) = 1 ) |
12 |
5 11
|
sylan9eqr |
⊢ ( ( 𝑛 ∈ ℤ ∧ ( 𝑛 · 2 ) = 𝑁 ) → ( - 1 ↑ 𝑁 ) = 1 ) |
13 |
12
|
rexlimiva |
⊢ ( ∃ 𝑛 ∈ ℤ ( 𝑛 · 2 ) = 𝑁 → ( - 1 ↑ 𝑁 ) = 1 ) |
14 |
3 13
|
syl6bi |
⊢ ( 𝑁 ∈ ℤ → ( 2 ∥ 𝑁 → ( - 1 ↑ 𝑁 ) = 1 ) ) |
15 |
14
|
impcom |
⊢ ( ( 2 ∥ 𝑁 ∧ 𝑁 ∈ ℤ ) → ( - 1 ↑ 𝑁 ) = 1 ) |
16 |
|
simpl |
⊢ ( ( 2 ∥ 𝑁 ∧ 𝑁 ∈ ℤ ) → 2 ∥ 𝑁 ) |
17 |
15 16
|
2thd |
⊢ ( ( 2 ∥ 𝑁 ∧ 𝑁 ∈ ℤ ) → ( ( - 1 ↑ 𝑁 ) = 1 ↔ 2 ∥ 𝑁 ) ) |
18 |
|
ax-1ne0 |
⊢ 1 ≠ 0 |
19 |
|
eqcom |
⊢ ( - 1 = 1 ↔ 1 = - 1 ) |
20 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
21 |
20
|
eqnegi |
⊢ ( 1 = - 1 ↔ 1 = 0 ) |
22 |
19 21
|
bitri |
⊢ ( - 1 = 1 ↔ 1 = 0 ) |
23 |
18 22
|
nemtbir |
⊢ ¬ - 1 = 1 |
24 |
|
odd2np1 |
⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) |
25 |
|
oveq2 |
⊢ ( 𝑁 = ( ( 2 · 𝑛 ) + 1 ) → ( - 1 ↑ 𝑁 ) = ( - 1 ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) |
26 |
25
|
eqcoms |
⊢ ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → ( - 1 ↑ 𝑁 ) = ( - 1 ↑ ( ( 2 · 𝑛 ) + 1 ) ) ) |
27 |
|
neg1cn |
⊢ - 1 ∈ ℂ |
28 |
27
|
a1i |
⊢ ( 𝑛 ∈ ℤ → - 1 ∈ ℂ ) |
29 |
|
neg1ne0 |
⊢ - 1 ≠ 0 |
30 |
29
|
a1i |
⊢ ( 𝑛 ∈ ℤ → - 1 ≠ 0 ) |
31 |
1
|
a1i |
⊢ ( 𝑛 ∈ ℤ → 2 ∈ ℤ ) |
32 |
|
id |
⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℤ ) |
33 |
31 32
|
zmulcld |
⊢ ( 𝑛 ∈ ℤ → ( 2 · 𝑛 ) ∈ ℤ ) |
34 |
28 30 33
|
expp1zd |
⊢ ( 𝑛 ∈ ℤ → ( - 1 ↑ ( ( 2 · 𝑛 ) + 1 ) ) = ( ( - 1 ↑ ( 2 · 𝑛 ) ) · - 1 ) ) |
35 |
10
|
oveq1d |
⊢ ( 𝑛 ∈ ℤ → ( ( - 1 ↑ ( 2 · 𝑛 ) ) · - 1 ) = ( 1 · - 1 ) ) |
36 |
27
|
mulid2i |
⊢ ( 1 · - 1 ) = - 1 |
37 |
35 36
|
eqtrdi |
⊢ ( 𝑛 ∈ ℤ → ( ( - 1 ↑ ( 2 · 𝑛 ) ) · - 1 ) = - 1 ) |
38 |
34 37
|
eqtrd |
⊢ ( 𝑛 ∈ ℤ → ( - 1 ↑ ( ( 2 · 𝑛 ) + 1 ) ) = - 1 ) |
39 |
26 38
|
sylan9eqr |
⊢ ( ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) → ( - 1 ↑ 𝑁 ) = - 1 ) |
40 |
39
|
rexlimiva |
⊢ ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → ( - 1 ↑ 𝑁 ) = - 1 ) |
41 |
24 40
|
syl6bi |
⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 → ( - 1 ↑ 𝑁 ) = - 1 ) ) |
42 |
41
|
impcom |
⊢ ( ( ¬ 2 ∥ 𝑁 ∧ 𝑁 ∈ ℤ ) → ( - 1 ↑ 𝑁 ) = - 1 ) |
43 |
42
|
eqeq1d |
⊢ ( ( ¬ 2 ∥ 𝑁 ∧ 𝑁 ∈ ℤ ) → ( ( - 1 ↑ 𝑁 ) = 1 ↔ - 1 = 1 ) ) |
44 |
23 43
|
mtbiri |
⊢ ( ( ¬ 2 ∥ 𝑁 ∧ 𝑁 ∈ ℤ ) → ¬ ( - 1 ↑ 𝑁 ) = 1 ) |
45 |
|
simpl |
⊢ ( ( ¬ 2 ∥ 𝑁 ∧ 𝑁 ∈ ℤ ) → ¬ 2 ∥ 𝑁 ) |
46 |
44 45
|
2falsed |
⊢ ( ( ¬ 2 ∥ 𝑁 ∧ 𝑁 ∈ ℤ ) → ( ( - 1 ↑ 𝑁 ) = 1 ↔ 2 ∥ 𝑁 ) ) |
47 |
17 46
|
pm2.61ian |
⊢ ( 𝑁 ∈ ℤ → ( ( - 1 ↑ 𝑁 ) = 1 ↔ 2 ∥ 𝑁 ) ) |