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 ∈ − 1 0 1 ↔ Z ≤ 1

Proof

Step Hyp Ref Expression
1 eltpi ⊢ Z ∈ − 1 0 1 → 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 ∈ − 1 0 1 → 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 ∈ − 1 0 1 ↔ Z = − 1 ∨ Z = 0 ∨ Z = 1
56 55 adantr ⊢ Z ∈ ℝ ∧ − 1 ≤ Z ∧ Z ≤ 1 → Z ∈ − 1 0 1 ↔ Z = − 1 ∨ Z = 0 ∨ Z = 1
57 56 adantl ⊢ Z = 0 ∨ Z ∈ ℕ ∨ − Z ∈ ℕ ∧ Z ∈ ℝ ∧ − 1 ≤ Z ∧ Z ≤ 1 → Z ∈ − 1 0 1 ↔ Z = − 1 ∨ Z = 0 ∨ Z = 1
58 54 57 mpbird ⊢ Z = 0 ∨ Z ∈ ℕ ∨ − Z ∈ ℕ ∧ Z ∈ ℝ ∧ − 1 ≤ Z ∧ Z ≤ 1 → Z ∈ − 1 0 1
59 58 exp32 ⊢ Z = 0 ∨ Z ∈ ℕ ∨ − Z ∈ ℕ → Z ∈ ℝ → − 1 ≤ Z ∧ Z ≤ 1 → Z ∈ − 1 0 1
60 59 impcom ⊢ Z ∈ ℝ ∧ Z = 0 ∨ Z ∈ ℕ ∨ − Z ∈ ℕ → − 1 ≤ Z ∧ Z ≤ 1 → Z ∈ − 1 0 1
61 23 60 sylbi ⊢ Z ∈ ℤ → − 1 ≤ Z ∧ Z ≤ 1 → Z ∈ − 1 0 1
62 22 61 sylbid ⊢ Z ∈ ℤ → Z ≤ 1 → Z ∈ − 1 0 1
63 19 62 impbid2 ⊢ Z ∈ ℤ → Z ∈ − 1 0 1 ↔ Z ≤ 1