Description: A member of a finite set of sequential integers is an integer. (Contributed by Glauco Siliprandi, 5Apr2020)
Ref  Expression  

Hypothesis  elfzelzd.1   ( ph > K e. ( M ... N ) ) 

Assertion  elfzelzd   ( ph > K e. ZZ ) 
Step  Hyp  Ref  Expression 

1  elfzelzd.1   ( ph > K e. ( M ... N ) ) 

2  elfzelz   ( K e. ( M ... N ) > K e. ZZ ) 

3  1 2  syl   ( ph > K e. ZZ ) 