This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 } )