Theorem fzssnn

Description: Finite sets of sequential integers starting from a natural are a subset of the positive integers. (Contributed by Thierry Arnoux, 4-Aug-2017)

	Ref	Expression
Assertion	fzssnn	⊢ ( 𝑀 ∈ ℕ → ( 𝑀 ... 𝑁 ) ⊆ ℕ )

Proof

Step	Hyp	Ref	Expression
1		fzss1	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 1 ) → ( 𝑀 ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) )
2		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
3	1 2	eleq2s	⊢ ( 𝑀 ∈ ℕ → ( 𝑀 ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) )
4		fz1ssnn	⊢ ( 1 ... 𝑁 ) ⊆ ℕ
5	3 4	sstrdi	⊢ ( 𝑀 ∈ ℕ → ( 𝑀 ... 𝑁 ) ⊆ ℕ )