This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fz1ssfz0

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

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

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