Theorem m1expeven

Description: Exponentiation of negative one to an even power. (Contributed by Scott Fenton, 17-Jan-2018)

	Ref	Expression
Assertion	m1expeven	⊢ ( 𝑁 ∈ ℤ → ( - 1 ↑ ( 2 · 𝑁 ) ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
2	1	2timesd	⊢ ( 𝑁 ∈ ℤ → ( 2 · 𝑁 ) = ( 𝑁 + 𝑁 ) )
3	2	oveq2d	⊢ ( 𝑁 ∈ ℤ → ( - 1 ↑ ( 2 · 𝑁 ) ) = ( - 1 ↑ ( 𝑁 + 𝑁 ) ) )
4		neg1cn	⊢ - 1 ∈ ℂ
5		neg1ne0	⊢ - 1 ≠ 0
6		expaddz	⊢ ( ( ( - 1 ∈ ℂ ∧ - 1 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( - 1 ↑ ( 𝑁 + 𝑁 ) ) = ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) )
7	4 5 6	mpanl12	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( - 1 ↑ ( 𝑁 + 𝑁 ) ) = ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) )
8	7	anidms	⊢ ( 𝑁 ∈ ℤ → ( - 1 ↑ ( 𝑁 + 𝑁 ) ) = ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) )
9		m1expcl2	⊢ ( 𝑁 ∈ ℤ → ( - 1 ↑ 𝑁 ) ∈ { - 1 , 1 } )
10		ovex	⊢ ( - 1 ↑ 𝑁 ) ∈ V
11	10	elpr	⊢ ( ( - 1 ↑ 𝑁 ) ∈ { - 1 , 1 } ↔ ( ( - 1 ↑ 𝑁 ) = - 1 ∨ ( - 1 ↑ 𝑁 ) = 1 ) )
12		oveq12	⊢ ( ( ( - 1 ↑ 𝑁 ) = - 1 ∧ ( - 1 ↑ 𝑁 ) = - 1 ) → ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) = ( - 1 · - 1 ) )
13	12	anidms	⊢ ( ( - 1 ↑ 𝑁 ) = - 1 → ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) = ( - 1 · - 1 ) )
14		neg1mulneg1e1	⊢ ( - 1 · - 1 ) = 1
15	13 14	eqtrdi	⊢ ( ( - 1 ↑ 𝑁 ) = - 1 → ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) = 1 )
16		oveq12	⊢ ( ( ( - 1 ↑ 𝑁 ) = 1 ∧ ( - 1 ↑ 𝑁 ) = 1 ) → ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) = ( 1 · 1 ) )
17	16	anidms	⊢ ( ( - 1 ↑ 𝑁 ) = 1 → ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) = ( 1 · 1 ) )
18		1t1e1	⊢ ( 1 · 1 ) = 1
19	17 18	eqtrdi	⊢ ( ( - 1 ↑ 𝑁 ) = 1 → ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) = 1 )
20	15 19	jaoi	⊢ ( ( ( - 1 ↑ 𝑁 ) = - 1 ∨ ( - 1 ↑ 𝑁 ) = 1 ) → ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) = 1 )
21	11 20	sylbi	⊢ ( ( - 1 ↑ 𝑁 ) ∈ { - 1 , 1 } → ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) = 1 )
22	9 21	syl	⊢ ( 𝑁 ∈ ℤ → ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) = 1 )
23	3 8 22	3eqtrd	⊢ ( 𝑁 ∈ ℤ → ( - 1 ↑ ( 2 · 𝑁 ) ) = 1 )