Metamath Proof Explorer


Theorem m1expcl2

Description: Closure of 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 syl5ibr
 |-  ( x = -u 1 -> ( y e. { -u 1 , 1 } -> ( x x. y ) e. { -u 1 , 1 } ) )
26 9 mulid2d
 |-  ( 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 syl5ibr
 |-  ( 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 } )