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 )