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 ... ( 𝑁 − 𝑀 ) ) )