This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database REAL AND COMPLEX NUMBERS Order sets Finite intervals of integers 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 ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 ... 𝑁 ) ⊆ ℕ )