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