This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrdi ⊢ ( 𝑁 ∈ ℤ → ( 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 mullidi ⊢ ( 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 biimtrdi ⊢ ( 𝑁 ∈ ℤ → ( ¬ 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 ∥ 𝑁 ) )