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 ) |