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

Metamath Proof Explorer

Theorem elfzmlbm

Description: Subtracting the lower bound of a finite set of sequential integers from an element of this set. (Contributed by Alexander van der Vekens, 29-Mar-2018) (Proof shortened by OpenAI, 25-Mar-2020)

Ref Expression
Assertion elfzmlbm ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 − 𝑀 ) ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 elfzuz ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )
2 uznn0sub ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐾 − 𝑀 ) ∈ ℕ0 )
3 1 2 syl ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 − 𝑀 ) ∈ ℕ0 )
4 elfzuz2 ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
5 uznn0sub ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 − 𝑀 ) ∈ ℕ0 )
6 4 5 syl ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝑁 − 𝑀 ) ∈ ℕ0 )
7 elfzelz ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝐾 ∈ ℤ )
8 7 zred ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝐾 ∈ ℝ )
9 elfzel2 ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ℤ )
10 9 zred ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ℝ )
11 elfzel1 ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝑀 ∈ ℤ )
12 11 zred ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝑀 ∈ ℝ )
13 elfzle2 ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝐾 ≤ 𝑁 )
14 8 10 12 13 lesub1dd ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 − 𝑀 ) ≤ ( 𝑁 − 𝑀 ) )
15 elfz2nn0 ⊢ ( ( 𝐾 − 𝑀 ) ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ↔ ( ( 𝐾 − 𝑀 ) ∈ ℕ0 ∧ ( 𝑁 − 𝑀 ) ∈ ℕ0 ∧ ( 𝐾 − 𝑀 ) ≤ ( 𝑁 − 𝑀 ) ) )
16 3 6 14 15 syl3anbrc ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 − 𝑀 ) ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) )