Metamath Proof Explorer


Theorem 0elfz

Description: 0 is an element of a finite set of sequential nonnegative integers with a nonnegative integer as upper bound. (Contributed by AV, 6-Apr-2018)

Ref Expression
Assertion 0elfz N 0 0 0 N

Proof

Step Hyp Ref Expression
1 0nn0 0 0
2 1 a1i N 0 0 0
3 id N 0 N 0
4 nn0ge0 N 0 0 N
5 elfz2nn0 0 0 N 0 0 N 0 0 N
6 2 3 4 5 syl3anbrc N 0 0 0 N