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

Metamath Proof Explorer

Theorem m1expoddALTV

Description: Exponentiation of -1 by an odd power. (Contributed by AV, 6-Jul-2020)

Ref Expression
Assertion m1expoddALTV ( 𝑁 ∈ Odd → ( - 1 ↑ 𝑁 ) = - 1 )

Proof

Step Hyp Ref Expression
1 oddz ⊢ ( 𝑁 ∈ Odd → 𝑁 ∈ ℤ )
2 1 zcnd ⊢ ( 𝑁 ∈ Odd → 𝑁 ∈ ℂ )
3 npcan1 ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
4 3 eqcomd ⊢ ( 𝑁 ∈ ℂ → 𝑁 = ( ( 𝑁 − 1 ) + 1 ) )
5 2 4 syl ⊢ ( 𝑁 ∈ Odd → 𝑁 = ( ( 𝑁 − 1 ) + 1 ) )
6 5 oveq2d ⊢ ( 𝑁 ∈ Odd → ( - 1 ↑ 𝑁 ) = ( - 1 ↑ ( ( 𝑁 − 1 ) + 1 ) ) )
7 neg1cn ⊢ - 1 ∈ ℂ
8 7 a1i ⊢ ( 𝑁 ∈ Odd → - 1 ∈ ℂ )
9 neg1ne0 ⊢ - 1 ≠ 0
10 9 a1i ⊢ ( 𝑁 ∈ Odd → - 1 ≠ 0 )
11 peano2zm ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
12 1 11 syl ⊢ ( 𝑁 ∈ Odd → ( 𝑁 − 1 ) ∈ ℤ )
13 8 10 12 expp1zd ⊢ ( 𝑁 ∈ Odd → ( - 1 ↑ ( ( 𝑁 − 1 ) + 1 ) ) = ( ( - 1 ↑ ( 𝑁 − 1 ) ) · - 1 ) )
14 oddm1eveni ⊢ ( 𝑁 ∈ Odd → ( 𝑁 − 1 ) ∈ Even )
15 m1expevenALTV ⊢ ( ( 𝑁 − 1 ) ∈ Even → ( - 1 ↑ ( 𝑁 − 1 ) ) = 1 )
16 14 15 syl ⊢ ( 𝑁 ∈ Odd → ( - 1 ↑ ( 𝑁 − 1 ) ) = 1 )
17 16 oveq1d ⊢ ( 𝑁 ∈ Odd → ( ( - 1 ↑ ( 𝑁 − 1 ) ) · - 1 ) = ( 1 · - 1 ) )
18 8 mullidd ⊢ ( 𝑁 ∈ Odd → ( 1 · - 1 ) = - 1 )
19 17 18 eqtrd ⊢ ( 𝑁 ∈ Odd → ( ( - 1 ↑ ( 𝑁 − 1 ) ) · - 1 ) = - 1 )
20 6 13 19 3eqtrd ⊢ ( 𝑁 ∈ Odd → ( - 1 ↑ 𝑁 ) = - 1 )