Metamath Proof Explorer

Theorem m1exp1

Description: Exponentiation of negative one is one iff the exponent is even. (Contributed by AV, 20-Jun-2021)

Ref Expression
Assertion m1exp1 ⊢ N ∈ ℤ → − 1 N = 1 ↔ 2 ∥ N

Proof

Step Hyp Ref Expression
1 2z ⊢ 2 ∈ ℤ
2 divides ⊢ 2 ∈ ℤ ∧ N ∈ ℤ → 2 ∥ N ↔ ∃ n ∈ ℤ n ⋅ 2 = N
3 1 2 mpan ⊢ N ∈ ℤ → 2 ∥ N ↔ ∃ n ∈ ℤ n ⋅ 2 = N
4 oveq2 ⊢ N = n ⋅ 2 → − 1 N = − 1 n ⋅ 2
5 4 eqcoms ⊢ n ⋅ 2 = N → − 1 N = − 1 n ⋅ 2
6 zcn ⊢ n ∈ ℤ → n ∈ ℂ
7 2cnd ⊢ n ∈ ℤ → 2 ∈ ℂ
8 6 7 mulcomd ⊢ n ∈ ℤ → n ⋅ 2 = 2 ⁢ n
9 8 oveq2d ⊢ n ∈ ℤ → − 1 n ⋅ 2 = − 1 2 ⁢ n
10 m1expeven ⊢ n ∈ ℤ → − 1 2 ⁢ n = 1
11 9 10 eqtrd ⊢ n ∈ ℤ → − 1 n ⋅ 2 = 1
12 5 11 sylan9eqr ⊢ n ∈ ℤ ∧ n ⋅ 2 = N → − 1 N = 1
13 12 rexlimiva ⊢ ∃ n ∈ ℤ n ⋅ 2 = N → − 1 N = 1
14 3 13 biimtrdi ⊢ N ∈ ℤ → 2 ∥ N → − 1 N = 1
15 14 impcom ⊢ 2 ∥ N ∧ N ∈ ℤ → − 1 N = 1
16 simpl ⊢ 2 ∥ N ∧ N ∈ ℤ → 2 ∥ N
17 15 16 2thd ⊢ 2 ∥ N ∧ N ∈ ℤ → − 1 N = 1 ↔ 2 ∥ N
18 ax-1ne0 ⊢ 1 ≠ 0
19 eqcom ⊢ − 1 = 1 ↔ 1 = − 1
20 ax-1cn ⊢ 1 ∈ ℂ
21 20 eqnegi ⊢ 1 = − 1 ↔ 1 = 0
22 19 21 bitri ⊢ − 1 = 1 ↔ 1 = 0
23 18 22 nemtbir ⊢ ¬ − 1 = 1
24 odd2np1 ⊢ N ∈ ℤ → ¬ 2 ∥ N ↔ ∃ n ∈ ℤ 2 ⁢ n + 1 = N
25 oveq2 ⊢ N = 2 ⁢ n + 1 → − 1 N = − 1 2 ⁢ n + 1
26 25 eqcoms ⊢ 2 ⁢ n + 1 = N → − 1 N = − 1 2 ⁢ n + 1
27 neg1cn ⊢ − 1 ∈ ℂ
28 27 a1i ⊢ n ∈ ℤ → − 1 ∈ ℂ
29 neg1ne0 ⊢ − 1 ≠ 0
30 29 a1i ⊢ n ∈ ℤ → − 1 ≠ 0
31 1 a1i ⊢ n ∈ ℤ → 2 ∈ ℤ
32 id ⊢ n ∈ ℤ → n ∈ ℤ
33 31 32 zmulcld ⊢ n ∈ ℤ → 2 ⁢ n ∈ ℤ
34 28 30 33 expp1zd ⊢ n ∈ ℤ → − 1 2 ⁢ n + 1 = − 1 2 ⁢ n ⁢ -1
35 10 oveq1d ⊢ n ∈ ℤ → − 1 2 ⁢ n ⁢ -1 = 1 ⁢ -1
36 27 mullidi ⊢ 1 ⁢ -1 = − 1
37 35 36 eqtrdi ⊢ n ∈ ℤ → − 1 2 ⁢ n ⁢ -1 = − 1
38 34 37 eqtrd ⊢ n ∈ ℤ → − 1 2 ⁢ n + 1 = − 1
39 26 38 sylan9eqr ⊢ n ∈ ℤ ∧ 2 ⁢ n + 1 = N → − 1 N = − 1
40 39 rexlimiva ⊢ ∃ n ∈ ℤ 2 ⁢ n + 1 = N → − 1 N = − 1
41 24 40 biimtrdi ⊢ N ∈ ℤ → ¬ 2 ∥ N → − 1 N = − 1
42 41 impcom ⊢ ¬ 2 ∥ N ∧ N ∈ ℤ → − 1 N = − 1
43 42 eqeq1d ⊢ ¬ 2 ∥ N ∧ N ∈ ℤ → − 1 N = 1 ↔ − 1 = 1
44 23 43 mtbiri ⊢ ¬ 2 ∥ N ∧ N ∈ ℤ → ¬ − 1 N = 1
45 simpl ⊢ ¬ 2 ∥ N ∧ N ∈ ℤ → ¬ 2 ∥ N
46 44 45 2falsed ⊢ ¬ 2 ∥ N ∧ N ∈ ℤ → − 1 N = 1 ↔ 2 ∥ N
47 17 46 pm2.61ian ⊢ N ∈ ℤ → − 1 N = 1 ↔ 2 ∥ N