Theorem m1expe

Description: Exponentiation of -1 by an even power. Variant of m1expeven . (Contributed by AV, 25-Jun-2021)

	Ref	Expression
Assertion	m1expe	⊢ ( 2 ∥ 𝑁 → ( - 1 ↑ 𝑁 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		even2n	⊢ ( 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( 2 · 𝑛 ) = 𝑁 )
2		oveq2	⊢ ( 𝑁 = ( 2 · 𝑛 ) → ( - 1 ↑ 𝑁 ) = ( - 1 ↑ ( 2 · 𝑛 ) ) )
3	2	eqcoms	⊢ ( ( 2 · 𝑛 ) = 𝑁 → ( - 1 ↑ 𝑁 ) = ( - 1 ↑ ( 2 · 𝑛 ) ) )
4		m1expeven	⊢ ( 𝑛 ∈ ℤ → ( - 1 ↑ ( 2 · 𝑛 ) ) = 1 )
5	3 4	sylan9eqr	⊢ ( ( 𝑛 ∈ ℤ ∧ ( 2 · 𝑛 ) = 𝑁 ) → ( - 1 ↑ 𝑁 ) = 1 )
6	5	rexlimiva	⊢ ( ∃ 𝑛 ∈ ℤ ( 2 · 𝑛 ) = 𝑁 → ( - 1 ↑ 𝑁 ) = 1 )
7	1 6	sylbi	⊢ ( 2 ∥ 𝑁 → ( - 1 ↑ 𝑁 ) = 1 )