Metamath Proof Explorer


Theorem m1expo

Description: Exponentiation of -1 by an odd power. (Contributed by AV, 26-Jun-2021)

Ref Expression
Assertion m1expo N ¬ 2 N 1 N = 1

Proof

Step Hyp Ref Expression
1 odd2np1 N ¬ 2 N n 2 n + 1 = N
2 oveq2 N = 2 n + 1 1 N = 1 2 n + 1
3 2 eqcoms 2 n + 1 = N 1 N = 1 2 n + 1
4 neg1cn 1
5 4 a1i n 1
6 neg1ne0 1 0
7 6 a1i n 1 0
8 2z 2
9 8 a1i n 2
10 id n n
11 9 10 zmulcld n 2 n
12 5 7 11 expp1zd n 1 2 n + 1 = 1 2 n -1
13 m1expeven n 1 2 n = 1
14 13 oveq1d n 1 2 n -1 = 1 -1
15 4 mulid2i 1 -1 = 1
16 14 15 eqtrdi n 1 2 n -1 = 1
17 12 16 eqtrd n 1 2 n + 1 = 1
18 17 adantl N n 1 2 n + 1 = 1
19 3 18 sylan9eqr N n 2 n + 1 = N 1 N = 1
20 19 rexlimdva2 N n 2 n + 1 = N 1 N = 1
21 1 20 sylbid N ¬ 2 N 1 N = 1
22 21 imp N ¬ 2 N 1 N = 1