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 syl6bir
 |-  ( 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 ) )