Metamath Proof Explorer


Theorem m1expcl2

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

Ref Expression
Assertion m1expcl2 ( ๐‘ โˆˆ โ„ค โ†’ ( - 1 โ†‘ ๐‘ ) โˆˆ { - 1 , 1 } )

Proof

Step Hyp Ref Expression
1 negex โŠข - 1 โˆˆ V
2 1 prid1 โŠข - 1 โˆˆ { - 1 , 1 }
3 neg1ne0 โŠข - 1 โ‰  0
4 neg1cn โŠข - 1 โˆˆ โ„‚
5 ax-1cn โŠข 1 โˆˆ โ„‚
6 prssi โŠข ( ( - 1 โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚ ) โ†’ { - 1 , 1 } โŠ† โ„‚ )
7 4 5 6 mp2an โŠข { - 1 , 1 } โŠ† โ„‚
8 elpri โŠข ( ๐‘ฅ โˆˆ { - 1 , 1 } โ†’ ( ๐‘ฅ = - 1 โˆจ ๐‘ฅ = 1 ) )
9 7 sseli โŠข ( ๐‘ฆ โˆˆ { - 1 , 1 } โ†’ ๐‘ฆ โˆˆ โ„‚ )
10 9 mulm1d โŠข ( ๐‘ฆ โˆˆ { - 1 , 1 } โ†’ ( - 1 ยท ๐‘ฆ ) = - ๐‘ฆ )
11 elpri โŠข ( ๐‘ฆ โˆˆ { - 1 , 1 } โ†’ ( ๐‘ฆ = - 1 โˆจ ๐‘ฆ = 1 ) )
12 negeq โŠข ( ๐‘ฆ = - 1 โ†’ - ๐‘ฆ = - - 1 )
13 negneg1e1 โŠข - - 1 = 1
14 1ex โŠข 1 โˆˆ V
15 14 prid2 โŠข 1 โˆˆ { - 1 , 1 }
16 13 15 eqeltri โŠข - - 1 โˆˆ { - 1 , 1 }
17 12 16 eqeltrdi โŠข ( ๐‘ฆ = - 1 โ†’ - ๐‘ฆ โˆˆ { - 1 , 1 } )
18 negeq โŠข ( ๐‘ฆ = 1 โ†’ - ๐‘ฆ = - 1 )
19 18 2 eqeltrdi โŠข ( ๐‘ฆ = 1 โ†’ - ๐‘ฆ โˆˆ { - 1 , 1 } )
20 17 19 jaoi โŠข ( ( ๐‘ฆ = - 1 โˆจ ๐‘ฆ = 1 ) โ†’ - ๐‘ฆ โˆˆ { - 1 , 1 } )
21 11 20 syl โŠข ( ๐‘ฆ โˆˆ { - 1 , 1 } โ†’ - ๐‘ฆ โˆˆ { - 1 , 1 } )
22 10 21 eqeltrd โŠข ( ๐‘ฆ โˆˆ { - 1 , 1 } โ†’ ( - 1 ยท ๐‘ฆ ) โˆˆ { - 1 , 1 } )
23 oveq1 โŠข ( ๐‘ฅ = - 1 โ†’ ( ๐‘ฅ ยท ๐‘ฆ ) = ( - 1 ยท ๐‘ฆ ) )
24 23 eleq1d โŠข ( ๐‘ฅ = - 1 โ†’ ( ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ { - 1 , 1 } โ†” ( - 1 ยท ๐‘ฆ ) โˆˆ { - 1 , 1 } ) )
25 22 24 imbitrrid โŠข ( ๐‘ฅ = - 1 โ†’ ( ๐‘ฆ โˆˆ { - 1 , 1 } โ†’ ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ { - 1 , 1 } ) )
26 9 mullidd โŠข ( ๐‘ฆ โˆˆ { - 1 , 1 } โ†’ ( 1 ยท ๐‘ฆ ) = ๐‘ฆ )
27 id โŠข ( ๐‘ฆ โˆˆ { - 1 , 1 } โ†’ ๐‘ฆ โˆˆ { - 1 , 1 } )
28 26 27 eqeltrd โŠข ( ๐‘ฆ โˆˆ { - 1 , 1 } โ†’ ( 1 ยท ๐‘ฆ ) โˆˆ { - 1 , 1 } )
29 oveq1 โŠข ( ๐‘ฅ = 1 โ†’ ( ๐‘ฅ ยท ๐‘ฆ ) = ( 1 ยท ๐‘ฆ ) )
30 29 eleq1d โŠข ( ๐‘ฅ = 1 โ†’ ( ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ { - 1 , 1 } โ†” ( 1 ยท ๐‘ฆ ) โˆˆ { - 1 , 1 } ) )
31 28 30 imbitrrid โŠข ( ๐‘ฅ = 1 โ†’ ( ๐‘ฆ โˆˆ { - 1 , 1 } โ†’ ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ { - 1 , 1 } ) )
32 25 31 jaoi โŠข ( ( ๐‘ฅ = - 1 โˆจ ๐‘ฅ = 1 ) โ†’ ( ๐‘ฆ โˆˆ { - 1 , 1 } โ†’ ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ { - 1 , 1 } ) )
33 8 32 syl โŠข ( ๐‘ฅ โˆˆ { - 1 , 1 } โ†’ ( ๐‘ฆ โˆˆ { - 1 , 1 } โ†’ ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ { - 1 , 1 } ) )
34 33 imp โŠข ( ( ๐‘ฅ โˆˆ { - 1 , 1 } โˆง ๐‘ฆ โˆˆ { - 1 , 1 } ) โ†’ ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ { - 1 , 1 } )
35 oveq2 โŠข ( ๐‘ฅ = - 1 โ†’ ( 1 / ๐‘ฅ ) = ( 1 / - 1 ) )
36 ax-1ne0 โŠข 1 โ‰  0
37 divneg2 โŠข ( ( 1 โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚ โˆง 1 โ‰  0 ) โ†’ - ( 1 / 1 ) = ( 1 / - 1 ) )
38 5 5 36 37 mp3an โŠข - ( 1 / 1 ) = ( 1 / - 1 )
39 1div1e1 โŠข ( 1 / 1 ) = 1
40 39 negeqi โŠข - ( 1 / 1 ) = - 1
41 38 40 eqtr3i โŠข ( 1 / - 1 ) = - 1
42 41 2 eqeltri โŠข ( 1 / - 1 ) โˆˆ { - 1 , 1 }
43 35 42 eqeltrdi โŠข ( ๐‘ฅ = - 1 โ†’ ( 1 / ๐‘ฅ ) โˆˆ { - 1 , 1 } )
44 oveq2 โŠข ( ๐‘ฅ = 1 โ†’ ( 1 / ๐‘ฅ ) = ( 1 / 1 ) )
45 39 15 eqeltri โŠข ( 1 / 1 ) โˆˆ { - 1 , 1 }
46 44 45 eqeltrdi โŠข ( ๐‘ฅ = 1 โ†’ ( 1 / ๐‘ฅ ) โˆˆ { - 1 , 1 } )
47 43 46 jaoi โŠข ( ( ๐‘ฅ = - 1 โˆจ ๐‘ฅ = 1 ) โ†’ ( 1 / ๐‘ฅ ) โˆˆ { - 1 , 1 } )
48 8 47 syl โŠข ( ๐‘ฅ โˆˆ { - 1 , 1 } โ†’ ( 1 / ๐‘ฅ ) โˆˆ { - 1 , 1 } )
49 48 adantr โŠข ( ( ๐‘ฅ โˆˆ { - 1 , 1 } โˆง ๐‘ฅ โ‰  0 ) โ†’ ( 1 / ๐‘ฅ ) โˆˆ { - 1 , 1 } )
50 7 34 15 49 expcl2lem โŠข ( ( - 1 โˆˆ { - 1 , 1 } โˆง - 1 โ‰  0 โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( - 1 โ†‘ ๐‘ ) โˆˆ { - 1 , 1 } )
51 2 3 50 mp3an12 โŠข ( ๐‘ โˆˆ โ„ค โ†’ ( - 1 โ†‘ ๐‘ ) โˆˆ { - 1 , 1 } )