Metamath Proof Explorer

Theorem m1expcl

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

Ref Expression
Assertion m1expcl ⊢ N ∈ ℤ → − 1 N ∈ ℤ

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 ⊢ N ∈ ℤ → − 1 N ∈ − 1 1
6 4 5 sseldi ⊢ N ∈ ℤ → − 1 N ∈ ℤ