# Metamath Proof Explorer

## Theorem m1expoddALTV

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

Ref Expression
Assertion m1expoddALTV ${⊢}{N}\in \mathrm{Odd}\to {\left(-1\right)}^{{N}}=-1$

### Proof

Step Hyp Ref Expression
1 oddz ${⊢}{N}\in \mathrm{Odd}\to {N}\in ℤ$
2 1 zcnd ${⊢}{N}\in \mathrm{Odd}\to {N}\in ℂ$
3 npcan1 ${⊢}{N}\in ℂ\to {N}-1+1={N}$
4 3 eqcomd ${⊢}{N}\in ℂ\to {N}={N}-1+1$
5 2 4 syl ${⊢}{N}\in \mathrm{Odd}\to {N}={N}-1+1$
6 5 oveq2d ${⊢}{N}\in \mathrm{Odd}\to {\left(-1\right)}^{{N}}={\left(-1\right)}^{{N}-1+1}$
7 neg1cn ${⊢}-1\in ℂ$
8 7 a1i ${⊢}{N}\in \mathrm{Odd}\to -1\in ℂ$
9 neg1ne0 ${⊢}-1\ne 0$
10 9 a1i ${⊢}{N}\in \mathrm{Odd}\to -1\ne 0$
11 peano2zm ${⊢}{N}\in ℤ\to {N}-1\in ℤ$
12 1 11 syl ${⊢}{N}\in \mathrm{Odd}\to {N}-1\in ℤ$
13 8 10 12 expp1zd ${⊢}{N}\in \mathrm{Odd}\to {\left(-1\right)}^{{N}-1+1}={\left(-1\right)}^{{N}-1}-1$
14 oddm1eveni ${⊢}{N}\in \mathrm{Odd}\to {N}-1\in \mathrm{Even}$
15 m1expevenALTV ${⊢}{N}-1\in \mathrm{Even}\to {\left(-1\right)}^{{N}-1}=1$
16 14 15 syl ${⊢}{N}\in \mathrm{Odd}\to {\left(-1\right)}^{{N}-1}=1$
17 16 oveq1d ${⊢}{N}\in \mathrm{Odd}\to {\left(-1\right)}^{{N}-1}-1=1-1$
18 8 mulid2d ${⊢}{N}\in \mathrm{Odd}\to 1-1=-1$
19 17 18 eqtrd ${⊢}{N}\in \mathrm{Odd}\to {\left(-1\right)}^{{N}-1}-1=-1$
20 6 13 19 3eqtrd ${⊢}{N}\in \mathrm{Odd}\to {\left(-1\right)}^{{N}}=-1$