Description: A nonnegative integer is less than or equal to twice itself. (Contributed by Raph Levien, 10-Dec-2002) (Proof shortened by AV, 9-Sep-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | nn0le2xi.1 | |- N e. NN0 |
|
| Assertion | nn0le2xi | |- N <_ ( 2 x. N ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nn0le2xi.1 | |- N e. NN0 |
|
| 2 | nn0le2x | |- ( N e. NN0 -> N <_ ( 2 x. N ) ) |
|
| 3 | 1 2 | ax-mp | |- N <_ ( 2 x. N ) |