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 ... 𝑁 ) )