Theorem fz2ssnn0

Description: A finite set of sequential integers that is a subset of NN0 . (Contributed by Thierry Arnoux, 8-Dec-2021)

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

Proof

Step	Hyp	Ref	Expression
1		fzssuz	⊢ ( 𝑀 ... 𝑁 ) ⊆ ( ℤ≥ ‘ 𝑀 )
2		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
3	2	eleq2i	⊢ ( 𝑀 ∈ ℕ0 ↔ 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
4	3	biimpi	⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
5		uzss	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) → ( ℤ≥ ‘ 𝑀 ) ⊆ ( ℤ≥ ‘ 0 ) )
6	4 5	syl	⊢ ( 𝑀 ∈ ℕ0 → ( ℤ≥ ‘ 𝑀 ) ⊆ ( ℤ≥ ‘ 0 ) )
7	6 2	sseqtrrdi	⊢ ( 𝑀 ∈ ℕ0 → ( ℤ≥ ‘ 𝑀 ) ⊆ ℕ0 )
8	1 7	sstrid	⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 ... 𝑁 ) ⊆ ℕ0 )