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