Metamath Proof Explorer


Theorem m1expe

Description: Exponentiation of -1 by an even power. Variant of m1expeven . (Contributed by AV, 25-Jun-2021)

Ref Expression
Assertion m1expe ( 2 ∥ 𝑁 → ( - 1 ↑ 𝑁 ) = 1 )

Proof

Step Hyp Ref Expression
1 even2n ( 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( 2 · 𝑛 ) = 𝑁 )
2 oveq2 ( 𝑁 = ( 2 · 𝑛 ) → ( - 1 ↑ 𝑁 ) = ( - 1 ↑ ( 2 · 𝑛 ) ) )
3 2 eqcoms ( ( 2 · 𝑛 ) = 𝑁 → ( - 1 ↑ 𝑁 ) = ( - 1 ↑ ( 2 · 𝑛 ) ) )
4 m1expeven ( 𝑛 ∈ ℤ → ( - 1 ↑ ( 2 · 𝑛 ) ) = 1 )
5 3 4 sylan9eqr ( ( 𝑛 ∈ ℤ ∧ ( 2 · 𝑛 ) = 𝑁 ) → ( - 1 ↑ 𝑁 ) = 1 )
6 5 rexlimiva ( ∃ 𝑛 ∈ ℤ ( 2 · 𝑛 ) = 𝑁 → ( - 1 ↑ 𝑁 ) = 1 )
7 1 6 sylbi ( 2 ∥ 𝑁 → ( - 1 ↑ 𝑁 ) = 1 )