Theorem m1expcl

Description: Closure of exponentiation of negative one. (Contributed by Mario Carneiro, 18-Jun-2015)

	Ref	Expression
Assertion	m1expcl	⊢ ( 𝑁 ∈ ℤ → ( - 1 ↑ 𝑁 ) ∈ ℤ )

Proof

Step	Hyp	Ref	Expression
1		neg1z	⊢ - 1 ∈ ℤ
2		1z	⊢ 1 ∈ ℤ
3		prssi	⊢ ( ( - 1 ∈ ℤ ∧ 1 ∈ ℤ ) → { - 1 , 1 } ⊆ ℤ )
4	1 2 3	mp2an	⊢ { - 1 , 1 } ⊆ ℤ
5		m1expcl2	⊢ ( 𝑁 ∈ ℤ → ( - 1 ↑ 𝑁 ) ∈ { - 1 , 1 } )
6	4 5	sseldi	⊢ ( 𝑁 ∈ ℤ → ( - 1 ↑ 𝑁 ) ∈ ℤ )