Metamath Proof Explorer

Theorem fznn0sub

Description: Subtraction closure for a member of a finite set of sequential integers. (Contributed by NM, 16-Sep-2005) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion fznn0sub K M N N K 0


Step Hyp Ref Expression
1 elfzuz3 K M N N K
2 uznn0sub N K N K 0
3 1 2 syl K M N N K 0