Description: If an element of a half-open integer range is not contained in the lower subrange, it must be in the upper subrange. (Contributed by Alexander van der Vekens, 30-Mar-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | elfzonelfzo | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfzo2 | |
|
2 | simpr | |
|
3 | eluzelz | |
|
4 | 3 | 3ad2ant1 | |
5 | 4 | ad2antrr | |
6 | eluzelre | |
|
7 | zre | |
|
8 | ltnle | |
|
9 | 6 7 8 | syl2an | |
10 | id | |
|
11 | 10 | 3expa | |
12 | elfzo2 | |
|
13 | 11 12 | sylibr | |
14 | 13 | ex | |
15 | 9 14 | sylbird | |
16 | 15 | con1d | |
17 | 16 | ex | |
18 | 17 | com23 | |
19 | 18 | 3ad2ant1 | |
20 | 19 | imp31 | |
21 | eluz2 | |
|
22 | 2 5 20 21 | syl3anbrc | |
23 | simpll2 | |
|
24 | simpll3 | |
|
25 | elfzo2 | |
|
26 | 22 23 24 25 | syl3anbrc | |
27 | 26 | ex | |
28 | 1 27 | sylanb | |
29 | 28 | com12 | |