Description: Exponentiation of negative one is one iff the exponent is even. (Contributed by AV, 20-Jun-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | m1exp1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2z | |
|
2 | divides | |
|
3 | 1 2 | mpan | |
4 | oveq2 | |
|
5 | 4 | eqcoms | |
6 | zcn | |
|
7 | 2cnd | |
|
8 | 6 7 | mulcomd | |
9 | 8 | oveq2d | |
10 | m1expeven | |
|
11 | 9 10 | eqtrd | |
12 | 5 11 | sylan9eqr | |
13 | 12 | rexlimiva | |
14 | 3 13 | syl6bi | |
15 | 14 | impcom | |
16 | simpl | |
|
17 | 15 16 | 2thd | |
18 | ax-1ne0 | |
|
19 | eqcom | |
|
20 | ax-1cn | |
|
21 | 20 | eqnegi | |
22 | 19 21 | bitri | |
23 | 18 22 | nemtbir | |
24 | odd2np1 | |
|
25 | oveq2 | |
|
26 | 25 | eqcoms | |
27 | neg1cn | |
|
28 | 27 | a1i | |
29 | neg1ne0 | |
|
30 | 29 | a1i | |
31 | 1 | a1i | |
32 | id | |
|
33 | 31 32 | zmulcld | |
34 | 28 30 33 | expp1zd | |
35 | 10 | oveq1d | |
36 | 27 | mulid2i | |
37 | 35 36 | eqtrdi | |
38 | 34 37 | eqtrd | |
39 | 26 38 | sylan9eqr | |
40 | 39 | rexlimiva | |
41 | 24 40 | syl6bi | |
42 | 41 | impcom | |
43 | 42 | eqeq1d | |
44 | 23 43 | mtbiri | |
45 | simpl | |
|
46 | 44 45 | 2falsed | |
47 | 17 46 | pm2.61ian | |