This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐾 ∈ ( 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 ... 𝑁 ) )