Theorem fzss1

Description: Subset relationship for finite sets of sequential integers. (Contributed by NM, 28-Sep-2005) (Proof shortened by Mario Carneiro, 28-Apr-2015)

	Ref	Expression
Assertion	fzss1	$$⊢K\in {\mathbb{Z}}_{\ge M}\to \left(K\dots N\right)\subseteq \left(M\dots N\right)$$

Proof

Step	Hyp	Ref	Expression
1		elfzuz	$$⊢k\in \left(K\dots N\right)\to k\in {\mathbb{Z}}_{\ge K}$$
2		id	$$⊢K\in {\mathbb{Z}}_{\ge M}\to K\in {\mathbb{Z}}_{\ge M}$$
3		uztrn	$$⊢\left(k\in {\mathbb{Z}}_{\ge K}\wedge K\in {\mathbb{Z}}_{\ge M}\right)\to k\in {\mathbb{Z}}_{\ge M}$$
4	1 2 3	syl2anr	$$⊢\left(K\in {\mathbb{Z}}_{\ge M}\wedge k\in \left(K\dots N\right)\right)\to k\in {\mathbb{Z}}_{\ge M}$$
5		elfzuz3	$$⊢k\in \left(K\dots N\right)\to N\in {\mathbb{Z}}_{\ge k}$$
6	5	adantl	$$⊢\left(K\in {\mathbb{Z}}_{\ge M}\wedge k\in \left(K\dots N\right)\right)\to N\in {\mathbb{Z}}_{\ge k}$$
7		elfzuzb	$$⊢k\in \left(M\dots N\right)\leftrightarrow \left(k\in {\mathbb{Z}}_{\ge M}\wedge N\in {\mathbb{Z}}_{\ge k}\right)$$
8	4 6 7	sylanbrc	$$⊢\left(K\in {\mathbb{Z}}_{\ge M}\wedge k\in \left(K\dots N\right)\right)\to k\in \left(M\dots N\right)$$
9	8	ex	$$⊢K\in {\mathbb{Z}}_{\ge M}\to \left(k\in \left(K\dots N\right)\to k\in \left(M\dots N\right)\right)$$
10	9	ssrdv	$$⊢K\in {\mathbb{Z}}_{\ge M}\to \left(K\dots N\right)\subseteq \left(M\dots N\right)$$