# Metamath Proof Explorer

## Theorem fznn0sub2

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

Ref Expression
Assertion fznn0sub2 ${⊢}{K}\in \left(0\dots {N}\right)\to {N}-{K}\in \left(0\dots {N}\right)$

### Proof

Step Hyp Ref Expression
1 elfzle1 ${⊢}{K}\in \left(0\dots {N}\right)\to 0\le {K}$
2 elfzel2 ${⊢}{K}\in \left(0\dots {N}\right)\to {N}\in ℤ$
3 elfzelz ${⊢}{K}\in \left(0\dots {N}\right)\to {K}\in ℤ$
4 zre ${⊢}{N}\in ℤ\to {N}\in ℝ$
5 zre ${⊢}{K}\in ℤ\to {K}\in ℝ$
6 subge02 ${⊢}\left({N}\in ℝ\wedge {K}\in ℝ\right)\to \left(0\le {K}↔{N}-{K}\le {N}\right)$
7 4 5 6 syl2an ${⊢}\left({N}\in ℤ\wedge {K}\in ℤ\right)\to \left(0\le {K}↔{N}-{K}\le {N}\right)$
8 2 3 7 syl2anc ${⊢}{K}\in \left(0\dots {N}\right)\to \left(0\le {K}↔{N}-{K}\le {N}\right)$
9 1 8 mpbid ${⊢}{K}\in \left(0\dots {N}\right)\to {N}-{K}\le {N}$
10 fznn0sub ${⊢}{K}\in \left(0\dots {N}\right)\to {N}-{K}\in {ℕ}_{0}$
11 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
12 10 11 eleqtrdi ${⊢}{K}\in \left(0\dots {N}\right)\to {N}-{K}\in {ℤ}_{\ge 0}$
13 elfz5 ${⊢}\left({N}-{K}\in {ℤ}_{\ge 0}\wedge {N}\in ℤ\right)\to \left({N}-{K}\in \left(0\dots {N}\right)↔{N}-{K}\le {N}\right)$
14 12 2 13 syl2anc ${⊢}{K}\in \left(0\dots {N}\right)\to \left({N}-{K}\in \left(0\dots {N}\right)↔{N}-{K}\le {N}\right)$
15 9 14 mpbird ${⊢}{K}\in \left(0\dots {N}\right)\to {N}-{K}\in \left(0\dots {N}\right)$