Metamath Proof Explorer


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 M0M..^N0

Proof

Step Hyp Ref Expression
1 fzossfz M..^NMN
2 fzss1 M0MN0N
3 nn0uz 0=0
4 2 3 eleq2s M0MN0N
5 1 4 sstrid M0M..^N0N
6 fz0ssnn0 0N0
7 5 6 sstrdi M0M..^N0