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 ∥ N → − 1 N = 1

Proof

Step Hyp Ref Expression
1 even2n ⊢ 2 ∥ N ↔ ∃ n ∈ ℤ 2 ⁢ n = N
2 oveq2 ⊢ N = 2 ⁢ n → − 1 N = − 1 2 ⁢ n
3 2 eqcoms ⊢ 2 ⁢ n = N → − 1 N = − 1 2 ⁢ n
4 m1expeven ⊢ n ∈ ℤ → − 1 2 ⁢ n = 1
5 3 4 sylan9eqr ⊢ n ∈ ℤ ∧ 2 ⁢ n = N → − 1 N = 1
6 5 rexlimiva ⊢ ∃ n ∈ ℤ 2 ⁢ n = N → − 1 N = 1
7 1 6 sylbi ⊢ 2 ∥ N → − 1 N = 1