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 e. ZZ -> ( Z e. { -u 1 , 0 , 1 } <-> ( abs ` Z ) <_ 1 ) )

Proof

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