Step |
Hyp |
Ref |
Expression |
1 |
|
zcn |
⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ ) |
2 |
1
|
2timesd |
⊢ ( 𝑁 ∈ ℤ → ( 2 · 𝑁 ) = ( 𝑁 + 𝑁 ) ) |
3 |
2
|
oveq2d |
⊢ ( 𝑁 ∈ ℤ → ( - 1 ↑ ( 2 · 𝑁 ) ) = ( - 1 ↑ ( 𝑁 + 𝑁 ) ) ) |
4 |
|
neg1cn |
⊢ - 1 ∈ ℂ |
5 |
|
neg1ne0 |
⊢ - 1 ≠ 0 |
6 |
|
expaddz |
⊢ ( ( ( - 1 ∈ ℂ ∧ - 1 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( - 1 ↑ ( 𝑁 + 𝑁 ) ) = ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) ) |
7 |
4 5 6
|
mpanl12 |
⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( - 1 ↑ ( 𝑁 + 𝑁 ) ) = ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) ) |
8 |
7
|
anidms |
⊢ ( 𝑁 ∈ ℤ → ( - 1 ↑ ( 𝑁 + 𝑁 ) ) = ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) ) |
9 |
|
m1expcl2 |
⊢ ( 𝑁 ∈ ℤ → ( - 1 ↑ 𝑁 ) ∈ { - 1 , 1 } ) |
10 |
|
ovex |
⊢ ( - 1 ↑ 𝑁 ) ∈ V |
11 |
10
|
elpr |
⊢ ( ( - 1 ↑ 𝑁 ) ∈ { - 1 , 1 } ↔ ( ( - 1 ↑ 𝑁 ) = - 1 ∨ ( - 1 ↑ 𝑁 ) = 1 ) ) |
12 |
|
oveq12 |
⊢ ( ( ( - 1 ↑ 𝑁 ) = - 1 ∧ ( - 1 ↑ 𝑁 ) = - 1 ) → ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) = ( - 1 · - 1 ) ) |
13 |
12
|
anidms |
⊢ ( ( - 1 ↑ 𝑁 ) = - 1 → ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) = ( - 1 · - 1 ) ) |
14 |
|
neg1mulneg1e1 |
⊢ ( - 1 · - 1 ) = 1 |
15 |
13 14
|
eqtrdi |
⊢ ( ( - 1 ↑ 𝑁 ) = - 1 → ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) = 1 ) |
16 |
|
oveq12 |
⊢ ( ( ( - 1 ↑ 𝑁 ) = 1 ∧ ( - 1 ↑ 𝑁 ) = 1 ) → ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) = ( 1 · 1 ) ) |
17 |
16
|
anidms |
⊢ ( ( - 1 ↑ 𝑁 ) = 1 → ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) = ( 1 · 1 ) ) |
18 |
|
1t1e1 |
⊢ ( 1 · 1 ) = 1 |
19 |
17 18
|
eqtrdi |
⊢ ( ( - 1 ↑ 𝑁 ) = 1 → ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) = 1 ) |
20 |
15 19
|
jaoi |
⊢ ( ( ( - 1 ↑ 𝑁 ) = - 1 ∨ ( - 1 ↑ 𝑁 ) = 1 ) → ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) = 1 ) |
21 |
11 20
|
sylbi |
⊢ ( ( - 1 ↑ 𝑁 ) ∈ { - 1 , 1 } → ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) = 1 ) |
22 |
9 21
|
syl |
⊢ ( 𝑁 ∈ ℤ → ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) = 1 ) |
23 |
3 8 22
|
3eqtrd |
⊢ ( 𝑁 ∈ ℤ → ( - 1 ↑ ( 2 · 𝑁 ) ) = 1 ) |