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∈ℤ→−1N∈−11

Proof

Step Hyp Ref Expression
1 negex ⊢−1∈V
2 1 prid1 ⊢−1∈−11
3 neg1ne0 ⊢−1≠0
4 neg1cn ⊢−1∈ℂ
5 ax-1cn ⊢1∈ℂ
6 prssi ⊢−1∈ℂ∧1∈ℂ→−11⊆ℂ
7 4 5 6 mp2an ⊢−11⊆ℂ
8 elpri ⊢x∈−11→x=−1∨x=1
9 7 sseli ⊢y∈−11→y∈ℂ
10 9 mulm1d ⊢y∈−11→-1⁢y=−y
11 elpri ⊢y∈−11→y=−1∨y=1
12 negeq ⊢y=−1→−y=−-1
13 negneg1e1 ⊢−-1=1
14 1ex ⊢1∈V
15 14 prid2 ⊢1∈−11
16 13 15 eqeltri ⊢−-1∈−11
17 12 16 eqeltrdi ⊢y=−1→−y∈−11
18 negeq ⊢y=1→−y=−1
19 18 2 eqeltrdi ⊢y=1→−y∈−11
20 17 19 jaoi ⊢y=−1∨y=1→−y∈−11
21 11 20 syl ⊢y∈−11→−y∈−11
22 10 21 eqeltrd ⊢y∈−11→-1⁢y∈−11
23 oveq1 ⊢x=−1→x⁢y=-1⁢y
24 23 eleq1d ⊢x=−1→x⁢y∈−11↔-1⁢y∈−11
25 22 24 imbitrrid ⊢x=−1→y∈−11→x⁢y∈−11
26 9 mullidd ⊢y∈−11→1⁢y=y
27 id ⊢y∈−11→y∈−11
28 26 27 eqeltrd ⊢y∈−11→1⁢y∈−11
29 oveq1 ⊢x=1→x⁢y=1⁢y
30 29 eleq1d ⊢x=1→x⁢y∈−11↔1⁢y∈−11
31 28 30 imbitrrid ⊢x=1→y∈−11→x⁢y∈−11
32 25 31 jaoi ⊢x=−1∨x=1→y∈−11→x⁢y∈−11
33 8 32 syl ⊢x∈−11→y∈−11→x⁢y∈−11
34 33 imp ⊢x∈−11∧y∈−11→x⁢y∈−11
35 oveq2 ⊢x=−1→1x=1−1
36 ax-1ne0 ⊢1≠0
37 divneg2 ⊢1∈ℂ∧1∈ℂ∧1≠0→−11=1−1
38 5 5 36 37 mp3an ⊢−11=1−1
39 1div1e1 ⊢11=1
40 39 negeqi ⊢−11=−1
41 38 40 eqtr3i ⊢1−1=−1
42 41 2 eqeltri ⊢1−1∈−11
43 35 42 eqeltrdi ⊢x=−1→1x∈−11
44 oveq2 ⊢x=1→1x=11
45 39 15 eqeltri ⊢11∈−11
46 44 45 eqeltrdi ⊢x=1→1x∈−11
47 43 46 jaoi ⊢x=−1∨x=1→1x∈−11
48 8 47 syl ⊢x∈−11→1x∈−11
49 48 adantr ⊢x∈−11∧x≠0→1x∈−11
50 7 34 15 49 expcl2lem ⊢−1∈−11∧−1≠0∧N∈ℤ→−1N∈−11
51 2 3 50 mp3an12 ⊢N∈ℤ→−1N∈−11