Metamath Proof Explorer

Theorem m1expcl

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

Ref Expression
Assertion m1expcl 
|- ( N e. ZZ -> ( -u 1 ^ N ) e. ZZ )

Proof

Step Hyp Ref Expression
1 neg1z 
 |-  -u 1 e. ZZ
2 1z 
 |-  1 e. ZZ
3 prssi 
 |-  ( ( -u 1 e. ZZ /\ 1 e. ZZ ) -> { -u 1 , 1 } C_ ZZ )
4 1 2 3 mp2an 
 |-  { -u 1 , 1 } C_ ZZ
5 m1expcl2 
 |-  ( N e. ZZ -> ( -u 1 ^ N ) e. { -u 1 , 1 } )
6 4 5 sselid 
 |-  ( N e. ZZ -> ( -u 1 ^ N ) e. ZZ )