Metamath Proof Explorer


Theorem elfzlble

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 NM0NNMN

Proof

Step Hyp Ref Expression
1 nn0z M0M
2 zsubcl NMNM
3 1 2 sylan2 NM0NM
4 simpl NM0N
5 nn0ge0 M00M
6 5 adantl NM00M
7 zre NN
8 nn0re M0M
9 subge02 NM0MNMN
10 7 8 9 syl2an NM00MNMN
11 6 10 mpbid NM0NMN
12 eluz2 NNMNMNNMN
13 3 4 11 12 syl3anbrc NM0NNM
14 eluzfz2 NNMNNMN
15 13 14 syl NM0NNMN