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 )