Description: An extended nonnegative integer is greater than or equal to 0. (Contributed by Alexander van der Vekens, 6-Jan-2018) (Revised by AV, 10-Dec-2020)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | xnn0ge0 | |- ( N e. NN0* -> 0 <_ N ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elxnn0 | |- ( N e. NN0* <-> ( N e. NN0 \/ N = +oo ) ) |
|
| 2 | nn0ge0 | |- ( N e. NN0 -> 0 <_ N ) |
|
| 3 | 0lepnf | |- 0 <_ +oo |
|
| 4 | breq2 | |- ( N = +oo -> ( 0 <_ N <-> 0 <_ +oo ) ) |
|
| 5 | 3 4 | mpbiri | |- ( N = +oo -> 0 <_ N ) |
| 6 | 2 5 | jaoi | |- ( ( N e. NN0 \/ N = +oo ) -> 0 <_ N ) |
| 7 | 1 6 | sylbi | |- ( N e. NN0* -> 0 <_ N ) |