Description: Subtraction closure for a member of a finite set of sequential integers. (Contributed by NM, 16Sep2005) (Revised by Mario Carneiro, 28Apr2015)
Ref  Expression  

Assertion  fznn0sub   ( K e. ( M ... N ) > ( N  K ) e. NN0 ) 
Step  Hyp  Ref  Expression 

1  elfzuz3   ( K e. ( M ... N ) > N e. ( ZZ>= ` K ) ) 

2  uznn0sub   ( N e. ( ZZ>= ` K ) > ( N  K ) e. NN0 ) 

3  1 2  syl   ( K e. ( M ... N ) > ( N  K ) e. NN0 ) 