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 ∈ 0 … N → N − K ∈ 0 … N

Proof

Step Hyp Ref Expression
1 elfzle1 ⊢ K ∈ 0 … N → 0 ≤ K
2 elfzel2 ⊢ K ∈ 0 … N → N ∈ ℤ
3 elfzelz ⊢ K ∈ 0 … N → K ∈ ℤ
4 zre ⊢ N ∈ ℤ → N ∈ ℝ
5 zre ⊢ K ∈ ℤ → K ∈ ℝ
6 subge02 ⊢ N ∈ ℝ ∧ K ∈ ℝ → 0 ≤ K ↔ N − K ≤ N
7 4 5 6 syl2an ⊢ N ∈ ℤ ∧ K ∈ ℤ → 0 ≤ K ↔ N − K ≤ N
8 2 3 7 syl2anc ⊢ K ∈ 0 … N → 0 ≤ K ↔ N − K ≤ N
9 1 8 mpbid ⊢ K ∈ 0 … N → N − K ≤ N
10 fznn0sub ⊢ K ∈ 0 … N → N − K ∈ ℕ 0
11 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
12 10 11 eleqtrdi ⊢ K ∈ 0 … N → N − K ∈ ℤ ≥ 0
13 elfz5 ⊢ N − K ∈ ℤ ≥ 0 ∧ N ∈ ℤ → N − K ∈ 0 … N ↔ N − K ≤ N
14 12 2 13 syl2anc ⊢ K ∈ 0 … N → N − K ∈ 0 … N ↔ N − K ≤ N
15 9 14 mpbird ⊢ K ∈ 0 … N → N − K ∈ 0 … N