Description: Membership of the difference of integers in a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 17-Sep-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | eluzgtdifelfzo | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl | |
|
2 | 1 | adantl | |
3 | simpl | |
|
4 | 3 | adantr | |
5 | eluzelz | |
|
6 | 5 | ad2antrr | |
7 | simprr | |
|
8 | 6 7 | zsubcld | |
9 | 8 | ancoms | |
10 | 4 9 | zaddcld | |
11 | zre | |
|
12 | zre | |
|
13 | posdif | |
|
14 | 13 | biimpd | |
15 | 11 12 14 | syl2anr | |
16 | 15 | adantld | |
17 | 16 | imp | |
18 | resubcl | |
|
19 | 12 11 18 | syl2an | |
20 | 19 | adantr | |
21 | eluzelre | |
|
22 | 21 | ad2antrl | |
23 | 20 22 | ltaddposd | |
24 | 17 23 | mpbid | |
25 | zcn | |
|
26 | 25 | ad2antrr | |
27 | eluzelcn | |
|
28 | 27 | ad2antrl | |
29 | zcn | |
|
30 | 29 | adantl | |
31 | 30 | adantr | |
32 | addsub12 | |
|
33 | 32 | breq2d | |
34 | 26 28 31 33 | syl3anc | |
35 | 24 34 | mpbird | |
36 | elfzo2 | |
|
37 | 2 10 35 36 | syl3anbrc | |
38 | fzosubel3 | |
|
39 | 37 9 38 | syl2anc | |
40 | 39 | ex | |