Theorem m1exp1

Description: Exponentiation of negative one is one iff the exponent is even. (Contributed by AV, 20-Jun-2021)

	Ref	Expression
Assertion	m1exp1	⊢ ( 𝑁 ∈ ℤ → ( ( - 1 ↑ 𝑁 ) = 1 ↔ 2 ∥ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		2z	⊢ 2 ∈ ℤ
2		divides	⊢ ( ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 · 2 ) = 𝑁 ) )
3	1 2	mpan	⊢ ( 𝑁 ∈ ℤ → ( 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 · 2 ) = 𝑁 ) )
4		oveq2	⊢ ( 𝑁 = ( 𝑛 · 2 ) → ( - 1 ↑ 𝑁 ) = ( - 1 ↑ ( 𝑛 · 2 ) ) )
5	4	eqcoms	⊢ ( ( 𝑛 · 2 ) = 𝑁 → ( - 1 ↑ 𝑁 ) = ( - 1 ↑ ( 𝑛 · 2 ) ) )
6		zcn	⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℂ )
7		2cnd	⊢ ( 𝑛 ∈ ℤ → 2 ∈ ℂ )
8	6 7	mulcomd	⊢ ( 𝑛 ∈ ℤ → ( 𝑛 · 2 ) = ( 2 · 𝑛 ) )
9	8	oveq2d	⊢ ( 𝑛 ∈ ℤ → ( - 1 ↑ ( 𝑛 · 2 ) ) = ( - 1 ↑ ( 2 · 𝑛 ) ) )
10		m1expeven	⊢ ( 𝑛 ∈ ℤ → ( - 1 ↑ ( 2 · 𝑛 ) ) = 1 )
11	9 10	eqtrd	⊢ ( 𝑛 ∈ ℤ → ( - 1 ↑ ( 𝑛 · 2 ) ) = 1 )
12	5 11	sylan9eqr	⊢ ( ( 𝑛 ∈ ℤ ∧ ( 𝑛 · 2 ) = 𝑁 ) → ( - 1 ↑ 𝑁 ) = 1 )
13	12	rexlimiva	⊢ ( ∃ 𝑛 ∈ ℤ ( 𝑛 · 2 ) = 𝑁 → ( - 1 ↑ 𝑁 ) = 1 )
14	3 13	syl6bi	⊢ ( 𝑁 ∈ ℤ → ( 2 ∥ 𝑁 → ( - 1 ↑ 𝑁 ) = 1 ) )
15	14	impcom	⊢ ( ( 2 ∥ 𝑁 ∧ 𝑁 ∈ ℤ ) → ( - 1 ↑ 𝑁 ) = 1 )
16		simpl	⊢ ( ( 2 ∥ 𝑁 ∧ 𝑁 ∈ ℤ ) → 2 ∥ 𝑁 )
17	15 16	2thd	⊢ ( ( 2 ∥ 𝑁 ∧ 𝑁 ∈ ℤ ) → ( ( - 1 ↑ 𝑁 ) = 1 ↔ 2 ∥ 𝑁 ) )
18		ax-1ne0	⊢ 1 ≠ 0
19		eqcom	⊢ ( - 1 = 1 ↔ 1 = - 1 )
20		ax-1cn	⊢ 1 ∈ ℂ
21	20	eqnegi	⊢ ( 1 = - 1 ↔ 1 = 0 )
22	19 21	bitri	⊢ ( - 1 = 1 ↔ 1 = 0 )
23	18 22	nemtbir	⊢ ¬ - 1 = 1
24		odd2np1	⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )
25		oveq2	⊢ ( 𝑁 = ( ( 2 · 𝑛 ) + 1 ) → ( - 1 ↑ 𝑁 ) = ( - 1 ↑ ( ( 2 · 𝑛 ) + 1 ) ) )
26	25	eqcoms	⊢ ( ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → ( - 1 ↑ 𝑁 ) = ( - 1 ↑ ( ( 2 · 𝑛 ) + 1 ) ) )
27		neg1cn	⊢ - 1 ∈ ℂ
28	27	a1i	⊢ ( 𝑛 ∈ ℤ → - 1 ∈ ℂ )
29		neg1ne0	⊢ - 1 ≠ 0
30	29	a1i	⊢ ( 𝑛 ∈ ℤ → - 1 ≠ 0 )
31	1	a1i	⊢ ( 𝑛 ∈ ℤ → 2 ∈ ℤ )
32		id	⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℤ )
33	31 32	zmulcld	⊢ ( 𝑛 ∈ ℤ → ( 2 · 𝑛 ) ∈ ℤ )
34	28 30 33	expp1zd	⊢ ( 𝑛 ∈ ℤ → ( - 1 ↑ ( ( 2 · 𝑛 ) + 1 ) ) = ( ( - 1 ↑ ( 2 · 𝑛 ) ) · - 1 ) )
35	10	oveq1d	⊢ ( 𝑛 ∈ ℤ → ( ( - 1 ↑ ( 2 · 𝑛 ) ) · - 1 ) = ( 1 · - 1 ) )
36	27	mulid2i	⊢ ( 1 · - 1 ) = - 1
37	35 36	eqtrdi	⊢ ( 𝑛 ∈ ℤ → ( ( - 1 ↑ ( 2 · 𝑛 ) ) · - 1 ) = - 1 )
38	34 37	eqtrd	⊢ ( 𝑛 ∈ ℤ → ( - 1 ↑ ( ( 2 · 𝑛 ) + 1 ) ) = - 1 )
39	26 38	sylan9eqr	⊢ ( ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) → ( - 1 ↑ 𝑁 ) = - 1 )
40	39	rexlimiva	⊢ ( ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 → ( - 1 ↑ 𝑁 ) = - 1 )
41	24 40	syl6bi	⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 → ( - 1 ↑ 𝑁 ) = - 1 ) )
42	41	impcom	⊢ ( ( ¬ 2 ∥ 𝑁 ∧ 𝑁 ∈ ℤ ) → ( - 1 ↑ 𝑁 ) = - 1 )
43	42	eqeq1d	⊢ ( ( ¬ 2 ∥ 𝑁 ∧ 𝑁 ∈ ℤ ) → ( ( - 1 ↑ 𝑁 ) = 1 ↔ - 1 = 1 ) )
44	23 43	mtbiri	⊢ ( ( ¬ 2 ∥ 𝑁 ∧ 𝑁 ∈ ℤ ) → ¬ ( - 1 ↑ 𝑁 ) = 1 )
45		simpl	⊢ ( ( ¬ 2 ∥ 𝑁 ∧ 𝑁 ∈ ℤ ) → ¬ 2 ∥ 𝑁 )
46	44 45	2falsed	⊢ ( ( ¬ 2 ∥ 𝑁 ∧ 𝑁 ∈ ℤ ) → ( ( - 1 ↑ 𝑁 ) = 1 ↔ 2 ∥ 𝑁 ) )
47	17 46	pm2.61ian	⊢ ( 𝑁 ∈ ℤ → ( ( - 1 ↑ 𝑁 ) = 1 ↔ 2 ∥ 𝑁 ) )