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

Metamath Proof Explorer

Theorem m1expo

Description: Exponentiation of -1 by an odd power. (Contributed by AV, 26-Jun-2021)

Ref Expression
Assertion m1expo ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) → ( - 1 ↑ 𝑁 ) = - 1 )

Proof

Step Hyp Ref Expression
1 odd2np1 ⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )
2 oveq2 ⊢ ( 𝑁 = ( ( 2 · 𝑛 ) + 1 ) → ( - 1 ↑ 𝑁 ) = ( - 1 ↑ ( ( 2 · 𝑛 ) + 1 ) ) )
3 2 eqcoms ⊢ ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → ( - 1 ↑ 𝑁 ) = ( - 1 ↑ ( ( 2 · 𝑛 ) + 1 ) ) )
4 neg1cn ⊢ - 1 ∈ ℂ
5 4 a1i ⊢ ( 𝑛 ∈ ℤ → - 1 ∈ ℂ )
6 neg1ne0 ⊢ - 1 ≠ 0
7 6 a1i ⊢ ( 𝑛 ∈ ℤ → - 1 ≠ 0 )
8 2z ⊢ 2 ∈ ℤ
9 8 a1i ⊢ ( 𝑛 ∈ ℤ → 2 ∈ ℤ )
10 id ⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℤ )
11 9 10 zmulcld ⊢ ( 𝑛 ∈ ℤ → ( 2 · 𝑛 ) ∈ ℤ )
12 5 7 11 expp1zd ⊢ ( 𝑛 ∈ ℤ → ( - 1 ↑ ( ( 2 · 𝑛 ) + 1 ) ) = ( ( - 1 ↑ ( 2 · 𝑛 ) ) · - 1 ) )
13 m1expeven ⊢ ( 𝑛 ∈ ℤ → ( - 1 ↑ ( 2 · 𝑛 ) ) = 1 )
14 13 oveq1d ⊢ ( 𝑛 ∈ ℤ → ( ( - 1 ↑ ( 2 · 𝑛 ) ) · - 1 ) = ( 1 · - 1 ) )
15 4 mullidi ⊢ ( 1 · - 1 ) = - 1
16 14 15 eqtrdi ⊢ ( 𝑛 ∈ ℤ → ( ( - 1 ↑ ( 2 · 𝑛 ) ) · - 1 ) = - 1 )
17 12 16 eqtrd ⊢ ( 𝑛 ∈ ℤ → ( - 1 ↑ ( ( 2 · 𝑛 ) + 1 ) ) = - 1 )
18 17 adantl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( - 1 ↑ ( ( 2 · 𝑛 ) + 1 ) ) = - 1 )
19 3 18 sylan9eqr ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) → ( - 1 ↑ 𝑁 ) = - 1 )
20 19 rexlimdva2 ⊢ ( 𝑁 ∈ ℤ → ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → ( - 1 ↑ 𝑁 ) = - 1 ) )
21 1 20 sylbid ⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 → ( - 1 ↑ 𝑁 ) = - 1 ) )
22 21 imp ⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) → ( - 1 ↑ 𝑁 ) = - 1 )