Metamath Proof Explorer


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 ( 𝑀 ∈ ℕ → ( 𝑀 ... 𝑁 ) ⊆ ℕ )