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