Theorem fzp1ss

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

	Ref	Expression
Assertion	fzp1ss	$$⊢M\in \mathbb{Z}\to \left(M+1\dots N\right)\subseteq \left(M\dots N\right)$$

Proof

Step	Hyp	Ref	Expression
1		uzid	$$⊢M\in \mathbb{Z}\to M\in {\mathbb{Z}}_{\ge M}$$
2		peano2uz	$$⊢M\in {\mathbb{Z}}_{\ge M}\to M+1\in {\mathbb{Z}}_{\ge M}$$
3		fzss1	$$⊢M+1\in {\mathbb{Z}}_{\ge M}\to \left(M+1\dots N\right)\subseteq \left(M\dots N\right)$$
4	1 2 3	3syl	$$⊢M\in \mathbb{Z}\to \left(M+1\dots N\right)\subseteq \left(M\dots N\right)$$