Description: Nonnegative integers are a subset of the integers. (Contributed by NM, 9-May-2004)
Ref | Expression | ||
---|---|---|---|
Assertion | nn0ssz |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-n0 | ||
2 | nnssz | ||
3 | 0z | ||
4 | c0ex | ||
5 | 4 | snss | |
6 | 3 5 | mpbi | |
7 | 2 6 | unssi | |
8 | 1 7 | eqsstri |