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

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

Proof

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