Metamath Proof Explorer

Theorem zabsle1

Description: { -u 1 , 0 , 1 } is the set of all integers with absolute value at most 1 . (Contributed by AV, 13-Jul-2021)

Ref Expression
Assertion zabsle1 ⊢Z∈ℤ→Z∈−101↔Z≤1

Proof

Step Hyp Ref Expression
1 eltpi ⊢Z∈−101→Z=−1∨Z=0∨Z=1
2 fveq2 ⊢Z=−1→Z=−1
3 ax-1cn ⊢1∈ℂ
4 3 absnegi ⊢−1=1
5 abs1 ⊢1=1
6 4 5 eqtri ⊢−1=1
7 1le1 ⊢1≤1
8 6 7 eqbrtri ⊢−1≤1
9 2 8 eqbrtrdi ⊢Z=−1→Z≤1
10 fveq2 ⊢Z=0→Z=0
11 abs0 ⊢0=0
12 0le1 ⊢0≤1
13 11 12 eqbrtri ⊢0≤1
14 10 13 eqbrtrdi ⊢Z=0→Z≤1
15 fveq2 ⊢Z=1→Z=1
16 5 7 eqbrtri ⊢1≤1
17 15 16 eqbrtrdi ⊢Z=1→Z≤1
18 9 14 17 3jaoi ⊢Z=−1∨Z=0∨Z=1→Z≤1
19 1 18 syl ⊢Z∈−101→Z≤1
20 zre ⊢Z∈ℤ→Z∈ℝ
21 1red ⊢Z∈ℤ→1∈ℝ
22 20 21 absled ⊢Z∈ℤ→Z≤1↔−1≤Z∧Z≤1
23 elz ⊢Z∈ℤ↔Z∈ℝ∧Z=0∨Z∈ℕ∨−Z∈ℕ
24 3mix2 ⊢Z=0→Z=−1∨Z=0∨Z=1
25 24 a1d ⊢Z=0→Z∈ℝ∧−1≤Z∧Z≤1→Z=−1∨Z=0∨Z=1
26 nnle1eq1 ⊢Z∈ℕ→Z≤1↔Z=1
27 26 biimpac ⊢Z≤1∧Z∈ℕ→Z=1
28 27 3mix3d ⊢Z≤1∧Z∈ℕ→Z=−1∨Z=0∨Z=1
29 28 ex ⊢Z≤1→Z∈ℕ→Z=−1∨Z=0∨Z=1
30 29 adantl ⊢−1≤Z∧Z≤1→Z∈ℕ→Z=−1∨Z=0∨Z=1
31 30 adantl ⊢Z∈ℝ∧−1≤Z∧Z≤1→Z∈ℕ→Z=−1∨Z=0∨Z=1
32 31 com12 ⊢Z∈ℕ→Z∈ℝ∧−1≤Z∧Z≤1→Z=−1∨Z=0∨Z=1
33 elnnz1 ⊢−Z∈ℕ↔−Z∈ℤ∧1≤−Z
34 1red ⊢Z∈ℝ→1∈ℝ
35 lenegcon2 ⊢1∈ℝ∧Z∈ℝ→1≤−Z↔Z≤−1
36 34 35 mpancom ⊢Z∈ℝ→1≤−Z↔Z≤−1
37 neg1rr ⊢−1∈ℝ
38 37 a1i ⊢Z∈ℝ→−1∈ℝ
39 id ⊢Z∈ℝ→Z∈ℝ
40 38 39 letri3d ⊢Z∈ℝ→−1=Z↔−1≤Z∧Z≤−1
41 3mix1 ⊢Z=−1→Z=−1∨Z=0∨Z=1
42 41 eqcoms ⊢−1=Z→Z=−1∨Z=0∨Z=1
43 40 42 syl6bir ⊢Z∈ℝ→−1≤Z∧Z≤−1→Z=−1∨Z=0∨Z=1
44 43 com12 ⊢−1≤Z∧Z≤−1→Z∈ℝ→Z=−1∨Z=0∨Z=1
45 44 ex ⊢−1≤Z→Z≤−1→Z∈ℝ→Z=−1∨Z=0∨Z=1
46 45 adantr ⊢−1≤Z∧Z≤1→Z≤−1→Z∈ℝ→Z=−1∨Z=0∨Z=1
47 46 com13 ⊢Z∈ℝ→Z≤−1→−1≤Z∧Z≤1→Z=−1∨Z=0∨Z=1
48 36 47 sylbid ⊢Z∈ℝ→1≤−Z→−1≤Z∧Z≤1→Z=−1∨Z=0∨Z=1
49 48 com12 ⊢1≤−Z→Z∈ℝ→−1≤Z∧Z≤1→Z=−1∨Z=0∨Z=1
50 49 impd ⊢1≤−Z→Z∈ℝ∧−1≤Z∧Z≤1→Z=−1∨Z=0∨Z=1
51 50 adantl ⊢−Z∈ℤ∧1≤−Z→Z∈ℝ∧−1≤Z∧Z≤1→Z=−1∨Z=0∨Z=1
52 33 51 sylbi ⊢−Z∈ℕ→Z∈ℝ∧−1≤Z∧Z≤1→Z=−1∨Z=0∨Z=1
53 25 32 52 3jaoi ⊢Z=0∨Z∈ℕ∨−Z∈ℕ→Z∈ℝ∧−1≤Z∧Z≤1→Z=−1∨Z=0∨Z=1
54 53 imp ⊢Z=0∨Z∈ℕ∨−Z∈ℕ∧Z∈ℝ∧−1≤Z∧Z≤1→Z=−1∨Z=0∨Z=1
55 eltpg ⊢Z∈ℝ→Z∈−101↔Z=−1∨Z=0∨Z=1
56 55 adantr ⊢Z∈ℝ∧−1≤Z∧Z≤1→Z∈−101↔Z=−1∨Z=0∨Z=1
57 56 adantl ⊢Z=0∨Z∈ℕ∨−Z∈ℕ∧Z∈ℝ∧−1≤Z∧Z≤1→Z∈−101↔Z=−1∨Z=0∨Z=1
58 54 57 mpbird ⊢Z=0∨Z∈ℕ∨−Z∈ℕ∧Z∈ℝ∧−1≤Z∧Z≤1→Z∈−101
59 58 exp32 ⊢Z=0∨Z∈ℕ∨−Z∈ℕ→Z∈ℝ→−1≤Z∧Z≤1→Z∈−101
60 59 impcom ⊢Z∈ℝ∧Z=0∨Z∈ℕ∨−Z∈ℕ→−1≤Z∧Z≤1→Z∈−101
61 23 60 sylbi ⊢Z∈ℤ→−1≤Z∧Z≤1→Z∈−101
62 22 61 sylbid ⊢Z∈ℤ→Z≤1→Z∈−101
63 19 62 impbid2 ⊢Z∈ℤ→Z∈−101↔Z≤1