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→−1N=−1

Proof

Step Hyp Ref Expression
1 odd2np1 ⊢N∈ℤ→¬2∥N↔∃n∈ℤ2⁢n+1=N
2 oveq2 ⊢N=2⁢n+1→−1N=−12⁢n+1
3 2 eqcoms ⊢2⁢n+1=N→−1N=−12⁢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∈ℤ→−12⁢n+1=−12⁢n⁢-1
13 m1expeven ⊢n∈ℤ→−12⁢n=1
14 13 oveq1d ⊢n∈ℤ→−12⁢n⁢-1=1⁢-1
15 4 mullidi ⊢1⁢-1=−1
16 14 15 eqtrdi ⊢n∈ℤ→−12⁢n⁢-1=−1
17 12 16 eqtrd ⊢n∈ℤ→−12⁢n+1=−1
18 17 adantl ⊢N∈ℤ∧n∈ℤ→−12⁢n+1=−1
19 3 18 sylan9eqr ⊢N∈ℤ∧n∈ℤ∧2⁢n+1=N→−1N=−1
20 19 rexlimdva2 ⊢N∈ℤ→∃n∈ℤ2⁢n+1=N→−1N=−1
21 1 20 sylbid ⊢N∈ℤ→¬2∥N→−1N=−1
22 21 imp ⊢N∈ℤ∧¬2∥N→−1N=−1