Metamath Proof Explorer

Theorem ubmelfzo

Description: If an integer in a 1-based finite set of sequential integers is subtracted from the upper bound of this finite set of sequential integers, the result is contained in a half-open range of nonnegative integers with the same upper bound. (Contributed by AV, 18-Mar-2018) (Revised by AV, 30-Oct-2018)

Ref Expression
Assertion ubmelfzo ⊢ K ∈ 1 … N → N − K ∈ 0 ..^ N

Proof

Step Hyp Ref Expression
1 simp3 ⊢ K ∈ ℕ ∧ N ∈ ℕ ∧ K ≤ N → K ≤ N
2 nnnn0 ⊢ K ∈ ℕ → K ∈ ℕ 0
3 nnnn0 ⊢ N ∈ ℕ → N ∈ ℕ 0
4 2 3 anim12i ⊢ K ∈ ℕ ∧ N ∈ ℕ → K ∈ ℕ 0 ∧ N ∈ ℕ 0
5 4 3adant3 ⊢ K ∈ ℕ ∧ N ∈ ℕ ∧ K ≤ N → K ∈ ℕ 0 ∧ N ∈ ℕ 0
6 nn0sub ⊢ K ∈ ℕ 0 ∧ N ∈ ℕ 0 → K ≤ N ↔ N − K ∈ ℕ 0
7 5 6 syl ⊢ K ∈ ℕ ∧ N ∈ ℕ ∧ K ≤ N → K ≤ N ↔ N − K ∈ ℕ 0
8 1 7 mpbid ⊢ K ∈ ℕ ∧ N ∈ ℕ ∧ K ≤ N → N − K ∈ ℕ 0
9 simp2 ⊢ K ∈ ℕ ∧ N ∈ ℕ ∧ K ≤ N → N ∈ ℕ
10 nngt0 ⊢ K ∈ ℕ → 0 < K
11 10 3ad2ant1 ⊢ K ∈ ℕ ∧ N ∈ ℕ ∧ K ≤ N → 0 < K
12 nnre ⊢ K ∈ ℕ → K ∈ ℝ
13 nnre ⊢ N ∈ ℕ → N ∈ ℝ
14 12 13 anim12i ⊢ K ∈ ℕ ∧ N ∈ ℕ → K ∈ ℝ ∧ N ∈ ℝ
15 14 3adant3 ⊢ K ∈ ℕ ∧ N ∈ ℕ ∧ K ≤ N → K ∈ ℝ ∧ N ∈ ℝ
16 ltsubpos ⊢ K ∈ ℝ ∧ N ∈ ℝ → 0 < K ↔ N − K < N
17 15 16 syl ⊢ K ∈ ℕ ∧ N ∈ ℕ ∧ K ≤ N → 0 < K ↔ N − K < N
18 11 17 mpbid ⊢ K ∈ ℕ ∧ N ∈ ℕ ∧ K ≤ N → N − K < N
19 8 9 18 3jca ⊢ K ∈ ℕ ∧ N ∈ ℕ ∧ K ≤ N → N − K ∈ ℕ 0 ∧ N ∈ ℕ ∧ N − K < N
20 elfz1b ⊢ K ∈ 1 … N ↔ K ∈ ℕ ∧ N ∈ ℕ ∧ K ≤ N
21 elfzo0 ⊢ N − K ∈ 0 ..^ N ↔ N − K ∈ ℕ 0 ∧ N ∈ ℕ ∧ N − K < N
22 19 20 21 3imtr4i ⊢ K ∈ 1 … N → N − K ∈ 0 ..^ N