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	$⊢ K \in (M \dots N) \to K - M \in (0 \dots N - M)$

Proof

Step	Hyp	Ref	Expression
1		elfzuz	$⊢ K \in (M \dots N) \to K \in ℤ_{\geq M}$
2		uznn0sub	$⊢ K \in ℤ_{\geq M} \to K - M \in ℕ_{0}$
3	1 2	syl	$⊢ K \in (M \dots N) \to K - M \in ℕ_{0}$
4		elfzuz2	$⊢ K \in (M \dots N) \to N \in ℤ_{\geq M}$
5		uznn0sub	$⊢ N \in ℤ_{\geq M} \to N - M \in ℕ_{0}$
6	4 5	syl	$⊢ K \in (M \dots N) \to N - M \in ℕ_{0}$
7		elfzelz	$⊢ K \in (M \dots N) \to K \in ℤ$
8	7	zred	$⊢ K \in (M \dots N) \to K \in ℝ$
9		elfzel2	$⊢ K \in (M \dots N) \to N \in ℤ$
10	9	zred	$⊢ K \in (M \dots N) \to N \in ℝ$
11		elfzel1	$⊢ K \in (M \dots N) \to M \in ℤ$
12	11	zred	$⊢ K \in (M \dots N) \to M \in ℝ$
13		elfzle2	$⊢ K \in (M \dots N) \to K \leq N$
14	8 10 12 13	lesub1dd	$⊢ K \in (M \dots N) \to K - M \leq N - M$
15		elfz2nn0	$⊢ K - M \in (0 \dots N - M) \leftrightarrow (K - M \in ℕ_{0} \land N - M \in ℕ_{0} \land K - M \leq N - M)$
16	3 6 14 15	syl3anbrc	$⊢ K \in (M \dots N) \to K - M \in (0 \dots N - M)$