Theorem fz1ssfz0

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

	Ref	Expression
Assertion	fz1ssfz0	⊢ ( 1 ... 𝑁 ) ⊆ ( 0 ... 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		1e0p1	⊢ 1 = ( 0 + 1 )
2	1	oveq1i	⊢ ( 1 ... 𝑁 ) = ( ( 0 + 1 ) ... 𝑁 )
3		0z	⊢ 0 ∈ ℤ
4		fzp1ss	⊢ ( 0 ∈ ℤ → ( ( 0 + 1 ) ... 𝑁 ) ⊆ ( 0 ... 𝑁 ) )
5	3 4	ax-mp	⊢ ( ( 0 + 1 ) ... 𝑁 ) ⊆ ( 0 ... 𝑁 )
6	2 5	eqsstri	⊢ ( 1 ... 𝑁 ) ⊆ ( 0 ... 𝑁 )