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} ) |
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} ) |