Description: A member of a finite set of sequential nonnegative integers is a nonnegative integer. (Contributed by NM, 5Aug2005) (Revised by Mario Carneiro, 28Apr2015)
Ref  Expression  

Assertion  elfznn0   ( K e. ( 0 ... N ) > K e. NN0 ) 
Step  Hyp  Ref  Expression 

1  elfz2nn0   ( K e. ( 0 ... N ) <> ( K e. NN0 /\ N e. NN0 /\ K <_ N ) ) 

2  1  simp1bi   ( K e. ( 0 ... N ) > K e. NN0 ) 