Description: Membership in a finite set of sequential nonnegative integers. (Contributed by NM, 16-Sep-2005) (Revised by Mario Carneiro, 28-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | elfz2nn0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elnn0uz | |
|
2 | 1 | anbi1i | |
3 | eluznn0 | |
|
4 | eluzle | |
|
5 | 4 | adantl | |
6 | 3 5 | jca | |
7 | nn0z | |
|
8 | nn0z | |
|
9 | eluz | |
|
10 | 7 8 9 | syl2an | |
11 | 10 | biimprd | |
12 | 11 | impr | |
13 | 6 12 | impbida | |
14 | 13 | pm5.32i | |
15 | 2 14 | bitr3i | |
16 | elfzuzb | |
|
17 | 3anass | |
|
18 | 15 16 17 | 3bitr4i | |