Metamath Proof Explorer

Theorem m1expcl2

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

Ref Expression
Assertion m1expcl2 
|- ( N e. ZZ -> ( -u 1 ^ N ) e. { -u 1 , 1 } )

Proof

Step Hyp Ref Expression
1 negex 
 |-  -u 1 e. _V
2 1 prid1 
 |-  -u 1 e. { -u 1 , 1 }
3 neg1ne0 
 |-  -u 1 =/= 0
4 neg1cn 
 |-  -u 1 e. CC
5 ax-1cn 
 |-  1 e. CC
6 prssi 
 |-  ( ( -u 1 e. CC /\ 1 e. CC ) -> { -u 1 , 1 } C_ CC )
7 4 5 6 mp2an 
 |-  { -u 1 , 1 } C_ CC
8 elpri 
 |-  ( x e. { -u 1 , 1 } -> ( x = -u 1 \/ x = 1 ) )
9 7 sseli 
 |-  ( y e. { -u 1 , 1 } -> y e. CC )
10 9 mulm1d 
 |-  ( y e. { -u 1 , 1 } -> ( -u 1 x. y ) = -u y )
11 elpri 
 |-  ( y e. { -u 1 , 1 } -> ( y = -u 1 \/ y = 1 ) )
12 negeq 
 |-  ( y = -u 1 -> -u y = -u -u 1 )
13 negneg1e1 
 |-  -u -u 1 = 1
14 1ex 
 |-  1 e. _V
15 14 prid2 
 |-  1 e. { -u 1 , 1 }
16 13 15 eqeltri 
 |-  -u -u 1 e. { -u 1 , 1 }
17 12 16 eqeltrdi 
 |-  ( y = -u 1 -> -u y e. { -u 1 , 1 } )
18 negeq 
 |-  ( y = 1 -> -u y = -u 1 )
19 18 2 eqeltrdi 
 |-  ( y = 1 -> -u y e. { -u 1 , 1 } )
20 17 19 jaoi 
 |-  ( ( y = -u 1 \/ y = 1 ) -> -u y e. { -u 1 , 1 } )
21 11 20 syl 
 |-  ( y e. { -u 1 , 1 } -> -u y e. { -u 1 , 1 } )
22 10 21 eqeltrd 
 |-  ( y e. { -u 1 , 1 } -> ( -u 1 x. y ) e. { -u 1 , 1 } )
23 oveq1 
 |-  ( x = -u 1 -> ( x x. y ) = ( -u 1 x. y ) )
24 23 eleq1d 
 |-  ( x = -u 1 -> ( ( x x. y ) e. { -u 1 , 1 } <-> ( -u 1 x. y ) e. { -u 1 , 1 } ) )
25 22 24 imbitrrid 
 |-  ( x = -u 1 -> ( y e. { -u 1 , 1 } -> ( x x. y ) e. { -u 1 , 1 } ) )
26 9 mullidd 
 |-  ( y e. { -u 1 , 1 } -> ( 1 x. y ) = y )
27 id 
 |-  ( y e. { -u 1 , 1 } -> y e. { -u 1 , 1 } )
28 26 27 eqeltrd 
 |-  ( y e. { -u 1 , 1 } -> ( 1 x. y ) e. { -u 1 , 1 } )
29 oveq1 
 |-  ( x = 1 -> ( x x. y ) = ( 1 x. y ) )
30 29 eleq1d 
 |-  ( x = 1 -> ( ( x x. y ) e. { -u 1 , 1 } <-> ( 1 x. y ) e. { -u 1 , 1 } ) )
31 28 30 imbitrrid 
 |-  ( x = 1 -> ( y e. { -u 1 , 1 } -> ( x x. y ) e. { -u 1 , 1 } ) )
32 25 31 jaoi 
 |-  ( ( x = -u 1 \/ x = 1 ) -> ( y e. { -u 1 , 1 } -> ( x x. y ) e. { -u 1 , 1 } ) )
33 8 32 syl 
 |-  ( x e. { -u 1 , 1 } -> ( y e. { -u 1 , 1 } -> ( x x. y ) e. { -u 1 , 1 } ) )
34 33 imp 
 |-  ( ( x e. { -u 1 , 1 } /\ y e. { -u 1 , 1 } ) -> ( x x. y ) e. { -u 1 , 1 } )
35 oveq2 
 |-  ( x = -u 1 -> ( 1 / x ) = ( 1 / -u 1 ) )
36 ax-1ne0 
 |-  1 =/= 0
37 divneg2 
 |-  ( ( 1 e. CC /\ 1 e. CC /\ 1 =/= 0 ) -> -u ( 1 / 1 ) = ( 1 / -u 1 ) )
38 5 5 36 37 mp3an 
 |-  -u ( 1 / 1 ) = ( 1 / -u 1 )
39 1div1e1 
 |-  ( 1 / 1 ) = 1
40 39 negeqi 
 |-  -u ( 1 / 1 ) = -u 1
41 38 40 eqtr3i 
 |-  ( 1 / -u 1 ) = -u 1
42 41 2 eqeltri 
 |-  ( 1 / -u 1 ) e. { -u 1 , 1 }
43 35 42 eqeltrdi 
 |-  ( x = -u 1 -> ( 1 / x ) e. { -u 1 , 1 } )
44 oveq2 
 |-  ( x = 1 -> ( 1 / x ) = ( 1 / 1 ) )
45 39 15 eqeltri 
 |-  ( 1 / 1 ) e. { -u 1 , 1 }
46 44 45 eqeltrdi 
 |-  ( x = 1 -> ( 1 / x ) e. { -u 1 , 1 } )
47 43 46 jaoi 
 |-  ( ( x = -u 1 \/ x = 1 ) -> ( 1 / x ) e. { -u 1 , 1 } )
48 8 47 syl 
 |-  ( x e. { -u 1 , 1 } -> ( 1 / x ) e. { -u 1 , 1 } )
49 48 adantr 
 |-  ( ( x e. { -u 1 , 1 } /\ x =/= 0 ) -> ( 1 / x ) e. { -u 1 , 1 } )
50 7 34 15 49 expcl2lem 
 |-  ( ( -u 1 e. { -u 1 , 1 } /\ -u 1 =/= 0 /\ N e. ZZ ) -> ( -u 1 ^ N ) e. { -u 1 , 1 } )
51 2 3 50 mp3an12 
 |-  ( N e. ZZ -> ( -u 1 ^ N ) e. { -u 1 , 1 } )