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 ∈ ℤ → − 1 N ∈ − 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 ⊢ x ∈ − 1 1 → x = − 1 ∨ x = 1
9 7 sseli ⊢ y ∈ − 1 1 → y ∈ ℂ
10 9 mulm1d ⊢ y ∈ − 1 1 → -1 ⁢ y = − y
11 elpri ⊢ y ∈ − 1 1 → y = − 1 ∨ y = 1
12 negeq ⊢ y = − 1 → − y = − -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 ⊢ y = − 1 → − y ∈ − 1 1
18 negeq ⊢ y = 1 → − y = − 1
19 18 2 eqeltrdi ⊢ y = 1 → − y ∈ − 1 1
20 17 19 jaoi ⊢ y = − 1 ∨ y = 1 → − y ∈ − 1 1
21 11 20 syl ⊢ y ∈ − 1 1 → − y ∈ − 1 1
22 10 21 eqeltrd ⊢ y ∈ − 1 1 → -1 ⁢ y ∈ − 1 1
23 oveq1 ⊢ x = − 1 → x ⁢ y = -1 ⁢ y
24 23 eleq1d ⊢ x = − 1 → x ⁢ y ∈ − 1 1 ↔ -1 ⁢ y ∈ − 1 1
25 22 24 imbitrrid ⊢ x = − 1 → y ∈ − 1 1 → x ⁢ y ∈ − 1 1
26 9 mullidd ⊢ y ∈ − 1 1 → 1 ⁢ y = y
27 id ⊢ y ∈ − 1 1 → y ∈ − 1 1
28 26 27 eqeltrd ⊢ y ∈ − 1 1 → 1 ⁢ y ∈ − 1 1
29 oveq1 ⊢ x = 1 → x ⁢ y = 1 ⁢ y
30 29 eleq1d ⊢ x = 1 → x ⁢ y ∈ − 1 1 ↔ 1 ⁢ y ∈ − 1 1
31 28 30 imbitrrid ⊢ x = 1 → y ∈ − 1 1 → x ⁢ y ∈ − 1 1
32 25 31 jaoi ⊢ x = − 1 ∨ x = 1 → y ∈ − 1 1 → x ⁢ y ∈ − 1 1
33 8 32 syl ⊢ x ∈ − 1 1 → y ∈ − 1 1 → x ⁢ y ∈ − 1 1
34 33 imp ⊢ x ∈ − 1 1 ∧ y ∈ − 1 1 → x ⁢ y ∈ − 1 1
35 oveq2 ⊢ x = − 1 → 1 x = 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 ⊢ x = − 1 → 1 x ∈ − 1 1
44 oveq2 ⊢ x = 1 → 1 x = 1 1
45 39 15 eqeltri ⊢ 1 1 ∈ − 1 1
46 44 45 eqeltrdi ⊢ x = 1 → 1 x ∈ − 1 1
47 43 46 jaoi ⊢ x = − 1 ∨ x = 1 → 1 x ∈ − 1 1
48 8 47 syl ⊢ x ∈ − 1 1 → 1 x ∈ − 1 1
49 48 adantr ⊢ x ∈ − 1 1 ∧ x ≠ 0 → 1 x ∈ − 1 1
50 7 34 15 49 expcl2lem ⊢ − 1 ∈ − 1 1 ∧ − 1 ≠ 0 ∧ N ∈ ℤ → − 1 N ∈ − 1 1
51 2 3 50 mp3an12 ⊢ N ∈ ℤ → − 1 N ∈ − 1 1