Description: A value in a finite set of sequential integers is a border value if and only if it is not contained in the half-open integer range contained in the finite set of sequential integers. (Contributed by Alexander van der Vekens, 17-Jan-2018) (Revised by Thierry Arnoux, 22-Dec-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | elfznelfzob | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfznelfzo | |
|
2 | 1 | ex | |
3 | elfzole1 | |
|
4 | elfzolt2 | |
|
5 | elfzoel2 | |
|
6 | elfzoelz | |
|
7 | 0lt1 | |
|
8 | breq1 | |
|
9 | 7 8 | mpbiri | |
10 | zre | |
|
11 | 10 | adantl | |
12 | 1red | |
|
13 | 11 12 | ltnled | |
14 | 9 13 | syl5ib | |
15 | 14 | con2d | |
16 | zre | |
|
17 | ltlen | |
|
18 | 10 16 17 | syl2anr | |
19 | necom | |
|
20 | df-ne | |
|
21 | 19 20 | sylbb | |
22 | 21 | adantl | |
23 | 18 22 | syl6bi | |
24 | 23 | ex | |
25 | 24 | com23 | |
26 | 25 | impcom | |
27 | 26 | imp | |
28 | 15 27 | jctird | |
29 | 4 5 6 28 | syl21anc | |
30 | 3 29 | mpd | |
31 | ioran | |
|
32 | 30 31 | sylibr | |
33 | 32 | a1i | |
34 | 33 | con2d | |
35 | 2 34 | impbid | |