Theorem 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 {\mathbb{Z}}_{\ge K}\to \left(M\dots K\right)\subseteq \left(M\dots N\right)$$

Proof

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