Metamath Proof Explorer


Theorem elfz2nn0

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 K0NK0N0KN

Proof

Step Hyp Ref Expression
1 elnn0uz K0K0
2 1 anbi1i K0NKK0NK
3 eluznn0 K0NKN0
4 eluzle NKKN
5 4 adantl K0NKKN
6 3 5 jca K0NKN0KN
7 nn0z K0K
8 nn0z N0N
9 eluz KNNKKN
10 7 8 9 syl2an K0N0NKKN
11 10 biimprd K0N0KNNK
12 11 impr K0N0KNNK
13 6 12 impbida K0NKN0KN
14 13 pm5.32i K0NKK0N0KN
15 2 14 bitr3i K0NKK0N0KN
16 elfzuzb K0NK0NK
17 3anass K0N0KNK0N0KN
18 15 16 17 3bitr4i K0NK0N0KN