Description: A nonnegative integer is a nonnegative real number. (Contributed by AV, 24-May-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | nn0rp0 | |- ( N e. NN0 -> N e. ( 0 [,) +oo ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nn0re | |- ( N e. NN0 -> N e. RR ) |
|
2 | nn0ge0 | |- ( N e. NN0 -> 0 <_ N ) |
|
3 | elrege0 | |- ( N e. ( 0 [,) +oo ) <-> ( N e. RR /\ 0 <_ N ) ) |
|
4 | 1 2 3 | sylanbrc | |- ( N e. NN0 -> N e. ( 0 [,) +oo ) ) |