Theorem m1expevenALTV

Description: Exponentiation of -1 by an even power. (Contributed by Glauco Siliprandi, 29-Jun-2017) (Revised by AV, 6-Jul-2020)

	Ref	Expression
Assertion	m1expevenALTV	⊢ ( 𝑁 ∈ Even → ( - 1 ↑ 𝑁 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		eqeq1	⊢ ( 𝑛 = 𝑁 → ( 𝑛 = ( 2 · 𝑖 ) ↔ 𝑁 = ( 2 · 𝑖 ) ) )
2	1	rexbidv	⊢ ( 𝑛 = 𝑁 → ( ∃ 𝑖 ∈ ℤ 𝑛 = ( 2 · 𝑖 ) ↔ ∃ 𝑖 ∈ ℤ 𝑁 = ( 2 · 𝑖 ) ) )
3		dfeven4	⊢ Even = { 𝑛 ∈ ℤ ∣ ∃ 𝑖 ∈ ℤ 𝑛 = ( 2 · 𝑖 ) }
4	2 3	elrab2	⊢ ( 𝑁 ∈ Even ↔ ( 𝑁 ∈ ℤ ∧ ∃ 𝑖 ∈ ℤ 𝑁 = ( 2 · 𝑖 ) ) )
5		oveq2	⊢ ( 𝑁 = ( 2 · 𝑖 ) → ( - 1 ↑ 𝑁 ) = ( - 1 ↑ ( 2 · 𝑖 ) ) )
6		neg1cn	⊢ - 1 ∈ ℂ
7	6	a1i	⊢ ( 𝑖 ∈ ℤ → - 1 ∈ ℂ )
8		neg1ne0	⊢ - 1 ≠ 0
9	8	a1i	⊢ ( 𝑖 ∈ ℤ → - 1 ≠ 0 )
10		2z	⊢ 2 ∈ ℤ
11	10	a1i	⊢ ( 𝑖 ∈ ℤ → 2 ∈ ℤ )
12		id	⊢ ( 𝑖 ∈ ℤ → 𝑖 ∈ ℤ )
13		expmulz	⊢ ( ( ( - 1 ∈ ℂ ∧ - 1 ≠ 0 ) ∧ ( 2 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ) → ( - 1 ↑ ( 2 · 𝑖 ) ) = ( ( - 1 ↑ 2 ) ↑ 𝑖 ) )
14	7 9 11 12 13	syl22anc	⊢ ( 𝑖 ∈ ℤ → ( - 1 ↑ ( 2 · 𝑖 ) ) = ( ( - 1 ↑ 2 ) ↑ 𝑖 ) )
15		neg1sqe1	⊢ ( - 1 ↑ 2 ) = 1
16	15	oveq1i	⊢ ( ( - 1 ↑ 2 ) ↑ 𝑖 ) = ( 1 ↑ 𝑖 )
17		1exp	⊢ ( 𝑖 ∈ ℤ → ( 1 ↑ 𝑖 ) = 1 )
18	16 17	syl5eq	⊢ ( 𝑖 ∈ ℤ → ( ( - 1 ↑ 2 ) ↑ 𝑖 ) = 1 )
19	14 18	eqtrd	⊢ ( 𝑖 ∈ ℤ → ( - 1 ↑ ( 2 · 𝑖 ) ) = 1 )
20	19	adantl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( - 1 ↑ ( 2 · 𝑖 ) ) = 1 )
21	5 20	sylan9eqr	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ 𝑁 = ( 2 · 𝑖 ) ) → ( - 1 ↑ 𝑁 ) = 1 )
22	21	rexlimdva2	⊢ ( 𝑁 ∈ ℤ → ( ∃ 𝑖 ∈ ℤ 𝑁 = ( 2 · 𝑖 ) → ( - 1 ↑ 𝑁 ) = 1 ) )
23	22	imp	⊢ ( ( 𝑁 ∈ ℤ ∧ ∃ 𝑖 ∈ ℤ 𝑁 = ( 2 · 𝑖 ) ) → ( - 1 ↑ 𝑁 ) = 1 )
24	4 23	sylbi	⊢ ( 𝑁 ∈ Even → ( - 1 ↑ 𝑁 ) = 1 )