Theorem fz1ssfz0

Description: Subset relationship for finite sets of sequential integers. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Assertion	fz1ssfz0	$$⊢\left(1\dots N\right)\subseteq \left(0\dots N\right)$$

Proof

Step	Hyp	Ref	Expression
1		1e0p1	$$⊢1=0+1$$
2	1	oveq1i	$$⊢\left(1\dots N\right)=\left(0+1\dots N\right)$$
3		0z	$$⊢0\in \mathbb{Z}$$
4		fzp1ss	$$⊢0\in \mathbb{Z}\to \left(0+1\dots N\right)\subseteq \left(0\dots N\right)$$
5	3 4	ax-mp	$$⊢\left(0+1\dots N\right)\subseteq \left(0\dots N\right)$$
6	2 5	eqsstri	$$⊢\left(1\dots N\right)\subseteq \left(0\dots N\right)$$