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	mulid2i	⊢ ( 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 )