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 N12 N=1

Proof

Step Hyp Ref Expression
1 zcn NN
2 1 2timesd N2 N=N+N
3 2 oveq2d N12 N=1N+N
4 neg1cn 1
5 neg1ne0 10
6 expaddz 110NN1N+N=1N1N
7 4 5 6 mpanl12 NN1N+N=1N1N
8 7 anidms N1N+N=1N1N
9 m1expcl2 N1N11
10 ovex 1NV
11 10 elpr 1N111N=11N=1
12 oveq12 1N=11N=11N1N=-1-1
13 12 anidms 1N=11N1N=-1-1
14 neg1mulneg1e1 -1-1=1
15 13 14 eqtrdi 1N=11N1N=1
16 oveq12 1N=11N=11N1N=11
17 16 anidms 1N=11N1N=11
18 1t1e1 11=1
19 17 18 eqtrdi 1N=11N1N=1
20 15 19 jaoi 1N=11N=11N1N=1
21 11 20 sylbi 1N111N1N=1
22 9 21 syl N1N1N=1
23 3 8 22 3eqtrd N12 N=1