Description: Exponentiation of negative one to an even power. (Contributed by Scott Fenton, 17-Jan-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | m1expeven | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zcn | |
|
2 | 1 | 2timesd | |
3 | 2 | oveq2d | |
4 | neg1cn | |
|
5 | neg1ne0 | |
|
6 | expaddz | |
|
7 | 4 5 6 | mpanl12 | |
8 | 7 | anidms | |
9 | m1expcl2 | |
|
10 | ovex | |
|
11 | 10 | elpr | |
12 | oveq12 | |
|
13 | 12 | anidms | |
14 | neg1mulneg1e1 | |
|
15 | 13 14 | eqtrdi | |
16 | oveq12 | |
|
17 | 16 | anidms | |
18 | 1t1e1 | |
|
19 | 17 18 | eqtrdi | |
20 | 15 19 | jaoi | |
21 | 11 20 | sylbi | |
22 | 9 21 | syl | |
23 | 3 8 22 | 3eqtrd | |