This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem m1expeven

Description: Exponentiation of negative one to an even power. (Contributed by Scott Fenton, 17-Jan-2018)

Ref Expression
Assertion m1expeven ( 𝑁 ∈ ℤ → ( - 1 ↑ ( 2 · 𝑁 ) ) = 1 )

Proof

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 )