Theorem fzossnn0

Description: A half-open integer range starting at a nonnegative integer is a subset of the nonnegative integers. (Contributed by Alexander van der Vekens, 13-May-2018)

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

Proof

Step	Hyp	Ref	Expression
1		fzossfz	⊢ ( 𝑀 ..^ 𝑁 ) ⊆ ( 𝑀 ... 𝑁 )
2		fzss1	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) → ( 𝑀 ... 𝑁 ) ⊆ ( 0 ... 𝑁 ) )
3		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
4	2 3	eleq2s	⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 ... 𝑁 ) ⊆ ( 0 ... 𝑁 ) )
5	1 4	sstrid	⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 ..^ 𝑁 ) ⊆ ( 0 ... 𝑁 ) )
6		fz0ssnn0	⊢ ( 0 ... 𝑁 ) ⊆ ℕ0
7	5 6	sstrdi	⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 ..^ 𝑁 ) ⊆ ℕ0 )