Theorem m1expcl

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

	Ref	Expression
Assertion	m1expcl	$$⊢N\in \mathbb{Z}\to {\left(-1\right)}^N\in \mathbb{Z}$$

Proof

Step	Hyp	Ref	Expression
1		neg1z	$$⊢-1\in \mathbb{Z}$$
2		1z	$$⊢1\in \mathbb{Z}$$
3		prssi	$$⊢\left(-1\in \mathbb{Z}\wedge 1\in \mathbb{Z}\right)\to \left\{-1,1\right\}\subseteq \mathbb{Z}$$
4	1 2 3	mp2an	$$⊢\left\{-1,1\right\}\subseteq \mathbb{Z}$$
5		m1expcl2	$$⊢N\in \mathbb{Z}\to {\left(-1\right)}^N\in \left\{-1,1\right\}$$
6	4 5	sselid	$$⊢N\in \mathbb{Z}\to {\left(-1\right)}^N\in \mathbb{Z}$$