fzss2

Description: Subset relationship for finite sets of sequential integers. (Contributed by NM, 4-Oct-2005) (Revised by Mario Carneiro, 30-Apr-2015)

		Ref	Expression
	Assertion	fzss2	$⊢ N \in ℤ_{\geq K} \to (M \dots K) \subseteq (M \dots N)$

Step	Hyp	Ref	Expression
1		elfzuz	$⊢ k \in (M \dots K) \to k \in ℤ_{\geq M}$
2	1	adantl	$⊢ (N \in ℤ_{\geq K} \land k \in (M \dots K)) \to k \in ℤ_{\geq M}$
3		elfzuz3	$⊢ k \in (M \dots K) \to K \in ℤ_{\geq k}$
4		uztrn	$⊢ (N \in ℤ_{\geq K} \land K \in ℤ_{\geq k}) \to N \in ℤ_{\geq k}$
5	3 4	sylan2	$⊢ (N \in ℤ_{\geq K} \land k \in (M \dots K)) \to N \in ℤ_{\geq k}$
6		elfzuzb	$⊢ k \in (M \dots N) \leftrightarrow (k \in ℤ_{\geq M} \land N \in ℤ_{\geq k})$
7	2 5 6	sylanbrc	$⊢ (N \in ℤ_{\geq K} \land k \in (M \dots K)) \to k \in (M \dots N)$
8	7	ex	$⊢ N \in ℤ_{\geq K} \to (k \in (M \dots K) \to k \in (M \dots N))$
9	8	ssrdv	$⊢ N \in ℤ_{\geq K} \to (M \dots K) \subseteq (M \dots N)$

Metamath Proof Explorer