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 ( 𝑍 ∈ ℤ → ( 𝑍 ∈ { - 1 , 0 , 1 } ↔ ( abs ‘ 𝑍 ) ≤ 1 ) )

Proof

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