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 2N1N=1

Proof

Step Hyp Ref Expression
1 even2n 2Nn2n=N
2 oveq2 N=2n1N=12n
3 2 eqcoms 2n=N1N=12n
4 m1expeven n12n=1
5 3 4 sylan9eqr n2n=N1N=1
6 5 rexlimiva n2n=N1N=1
7 1 6 sylbi 2N1N=1