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	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 − 𝐾 ) ∈ ( 0 ... 𝑁 ) )

Proof

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