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 ( 𝑁 ∈ ℤ → ( ( - 1 ↑ 𝑁 ) = 1 ↔ 2 ∥ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 2z 2 ∈ ℤ
2 divides ( ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 · 2 ) = 𝑁 ) )
3 1 2 mpan ( 𝑁 ∈ ℤ → ( 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 · 2 ) = 𝑁 ) )
4 oveq2 ( 𝑁 = ( 𝑛 · 2 ) → ( - 1 ↑ 𝑁 ) = ( - 1 ↑ ( 𝑛 · 2 ) ) )
5 4 eqcoms ( ( 𝑛 · 2 ) = 𝑁 → ( - 1 ↑ 𝑁 ) = ( - 1 ↑ ( 𝑛 · 2 ) ) )
6 zcn ( 𝑛 ∈ ℤ → 𝑛 ∈ ℂ )
7 2cnd ( 𝑛 ∈ ℤ → 2 ∈ ℂ )
8 6 7 mulcomd ( 𝑛 ∈ ℤ → ( 𝑛 · 2 ) = ( 2 · 𝑛 ) )
9 8 oveq2d ( 𝑛 ∈ ℤ → ( - 1 ↑ ( 𝑛 · 2 ) ) = ( - 1 ↑ ( 2 · 𝑛 ) ) )
10 m1expeven ( 𝑛 ∈ ℤ → ( - 1 ↑ ( 2 · 𝑛 ) ) = 1 )
11 9 10 eqtrd ( 𝑛 ∈ ℤ → ( - 1 ↑ ( 𝑛 · 2 ) ) = 1 )
12 5 11 sylan9eqr ( ( 𝑛 ∈ ℤ ∧ ( 𝑛 · 2 ) = 𝑁 ) → ( - 1 ↑ 𝑁 ) = 1 )
13 12 rexlimiva ( ∃ 𝑛 ∈ ℤ ( 𝑛 · 2 ) = 𝑁 → ( - 1 ↑ 𝑁 ) = 1 )
14 3 13 syl6bi ( 𝑁 ∈ ℤ → ( 2 ∥ 𝑁 → ( - 1 ↑ 𝑁 ) = 1 ) )
15 14 impcom ( ( 2 ∥ 𝑁𝑁 ∈ ℤ ) → ( - 1 ↑ 𝑁 ) = 1 )
16 simpl ( ( 2 ∥ 𝑁𝑁 ∈ ℤ ) → 2 ∥ 𝑁 )
17 15 16 2thd ( ( 2 ∥ 𝑁𝑁 ∈ ℤ ) → ( ( - 1 ↑ 𝑁 ) = 1 ↔ 2 ∥ 𝑁 ) )
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 ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )
25 oveq2 ( 𝑁 = ( ( 2 · 𝑛 ) + 1 ) → ( - 1 ↑ 𝑁 ) = ( - 1 ↑ ( ( 2 · 𝑛 ) + 1 ) ) )
26 25 eqcoms ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → ( - 1 ↑ 𝑁 ) = ( - 1 ↑ ( ( 2 · 𝑛 ) + 1 ) ) )
27 neg1cn - 1 ∈ ℂ
28 27 a1i ( 𝑛 ∈ ℤ → - 1 ∈ ℂ )
29 neg1ne0 - 1 ≠ 0
30 29 a1i ( 𝑛 ∈ ℤ → - 1 ≠ 0 )
31 1 a1i ( 𝑛 ∈ ℤ → 2 ∈ ℤ )
32 id ( 𝑛 ∈ ℤ → 𝑛 ∈ ℤ )
33 31 32 zmulcld ( 𝑛 ∈ ℤ → ( 2 · 𝑛 ) ∈ ℤ )
34 28 30 33 expp1zd ( 𝑛 ∈ ℤ → ( - 1 ↑ ( ( 2 · 𝑛 ) + 1 ) ) = ( ( - 1 ↑ ( 2 · 𝑛 ) ) · - 1 ) )
35 10 oveq1d ( 𝑛 ∈ ℤ → ( ( - 1 ↑ ( 2 · 𝑛 ) ) · - 1 ) = ( 1 · - 1 ) )
36 27 mulid2i ( 1 · - 1 ) = - 1
37 35 36 eqtrdi ( 𝑛 ∈ ℤ → ( ( - 1 ↑ ( 2 · 𝑛 ) ) · - 1 ) = - 1 )
38 34 37 eqtrd ( 𝑛 ∈ ℤ → ( - 1 ↑ ( ( 2 · 𝑛 ) + 1 ) ) = - 1 )
39 26 38 sylan9eqr ( ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) → ( - 1 ↑ 𝑁 ) = - 1 )
40 39 rexlimiva ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → ( - 1 ↑ 𝑁 ) = - 1 )
41 24 40 syl6bi ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 → ( - 1 ↑ 𝑁 ) = - 1 ) )
42 41 impcom ( ( ¬ 2 ∥ 𝑁𝑁 ∈ ℤ ) → ( - 1 ↑ 𝑁 ) = - 1 )
43 42 eqeq1d ( ( ¬ 2 ∥ 𝑁𝑁 ∈ ℤ ) → ( ( - 1 ↑ 𝑁 ) = 1 ↔ - 1 = 1 ) )
44 23 43 mtbiri ( ( ¬ 2 ∥ 𝑁𝑁 ∈ ℤ ) → ¬ ( - 1 ↑ 𝑁 ) = 1 )
45 simpl ( ( ¬ 2 ∥ 𝑁𝑁 ∈ ℤ ) → ¬ 2 ∥ 𝑁 )
46 44 45 2falsed ( ( ¬ 2 ∥ 𝑁𝑁 ∈ ℤ ) → ( ( - 1 ↑ 𝑁 ) = 1 ↔ 2 ∥ 𝑁 ) )
47 17 46 pm2.61ian ( 𝑁 ∈ ℤ → ( ( - 1 ↑ 𝑁 ) = 1 ↔ 2 ∥ 𝑁 ) )