Metamath Proof Explorer


Theorem m1exp1

Description: Exponentiation of negative one is one iff the exponent is even. (Contributed by AV, 20-Jun-2021)

Ref Expression
Assertion m1exp1 N1N=12N

Proof

Step Hyp Ref Expression
1 2z 2
2 divides 2N2Nnn2=N
3 1 2 mpan N2Nnn2=N
4 oveq2 N=n21N=1n2
5 4 eqcoms n2=N1N=1n2
6 zcn nn
7 2cnd n2
8 6 7 mulcomd nn2=2n
9 8 oveq2d n1n2=12n
10 m1expeven n12n=1
11 9 10 eqtrd n1n2=1
12 5 11 sylan9eqr nn2=N1N=1
13 12 rexlimiva nn2=N1N=1
14 3 13 syl6bi N2N1N=1
15 14 impcom 2NN1N=1
16 simpl 2NN2N
17 15 16 2thd 2NN1N=12N
18 ax-1ne0 10
19 eqcom 1=11=1
20 ax-1cn 1
21 20 eqnegi 1=11=0
22 19 21 bitri 1=11=0
23 18 22 nemtbir ¬1=1
24 odd2np1 N¬2Nn2n+1=N
25 oveq2 N=2n+11N=12n+1
26 25 eqcoms 2n+1=N1N=12n+1
27 neg1cn 1
28 27 a1i n1
29 neg1ne0 10
30 29 a1i n10
31 1 a1i n2
32 id nn
33 31 32 zmulcld n2n
34 28 30 33 expp1zd n12n+1=12n-1
35 10 oveq1d n12n-1=1-1
36 27 mulid2i 1-1=1
37 35 36 eqtrdi n12n-1=1
38 34 37 eqtrd n12n+1=1
39 26 38 sylan9eqr n2n+1=N1N=1
40 39 rexlimiva n2n+1=N1N=1
41 24 40 syl6bi N¬2N1N=1
42 41 impcom ¬2NN1N=1
43 42 eqeq1d ¬2NN1N=11=1
44 23 43 mtbiri ¬2NN¬1N=1
45 simpl ¬2NN¬2N
46 44 45 2falsed ¬2NN1N=12N
47 17 46 pm2.61ian N1N=12N