fzssfzo

Description: Condition for an integer interval to be a subset of a half-open integer interval. (Contributed by Thierry Arnoux, 8-Oct-2018)

		Ref	Expression
	Assertion	fzssfzo	$⊢ K \in (M ..^N) \to (M \dots K) \subseteq (M ..^N)$

Step	Hyp	Ref	Expression
1		elfzoel2	$⊢ K \in (M ..^N) \to N \in ℤ$
2		fzoval	$⊢ N \in ℤ \to (M ..^N) = (M \dots N - 1)$
3	1 2	syl	$⊢ K \in (M ..^N) \to (M ..^N) = (M \dots N - 1)$
4	3	eleq2d	$⊢ K \in (M ..^N) \to (K \in (M ..^N) \leftrightarrow K \in (M \dots N - 1))$
5	4	ibi	$⊢ K \in (M ..^N) \to K \in (M \dots N - 1)$
6		elfzuz3	$⊢ K \in (M \dots N - 1) \to N - 1 \in ℤ_{\geq K}$
7		fzss2	$⊢ N - 1 \in ℤ_{\geq K} \to (M \dots K) \subseteq (M \dots N - 1)$
8	5 6 7	3syl	$⊢ K \in (M ..^N) \to (M \dots K) \subseteq (M \dots N - 1)$
9	8 3	sseqtrrd	$⊢ K \in (M ..^N) \to (M \dots K) \subseteq (M ..^N)$

Metamath Proof Explorer