Metamath Proof Explorer


Theorem m1expcl2

Description: Closure of 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 syl5ibr ( 𝑥 = - 1 → ( 𝑦 ∈ { - 1 , 1 } → ( 𝑥 · 𝑦 ) ∈ { - 1 , 1 } ) )
26 9 mulid2d ( 𝑦 ∈ { - 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 syl5ibr ( 𝑥 = 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 } )