Description: Membership of an integer in a finite set of sequential integers with the integer as upper bound and a lower bound less than or equal to the integer. (Contributed by AV, 21-Oct-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | elfzlble | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nn0z | |
|
2 | zsubcl | |
|
3 | 1 2 | sylan2 | |
4 | simpl | |
|
5 | nn0ge0 | |
|
6 | 5 | adantl | |
7 | zre | |
|
8 | nn0re | |
|
9 | subge02 | |
|
10 | 7 8 9 | syl2an | |
11 | 6 10 | mpbid | |
12 | eluz2 | |
|
13 | 3 4 11 12 | syl3anbrc | |
14 | eluzfz2 | |
|
15 | 13 14 | syl | |