Metamath Proof Explorer

Theorem m1expoddALTV

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

Ref Expression
Assertion m1expoddALTV ⊢ N ∈ Odd → − 1 N = − 1

Proof

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