Description: A nonnegative integer is less than or equal to twice itself. Generalization of nn0le2xi . (Contributed by Raph Levien, 10-Dec-2002) (Revised by AV, 9-Sep-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nn0le2x | |- ( N e. NN0 -> N <_ ( 2 x. N ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nn0re | |- ( N e. NN0 -> N e. RR ) |
|
| 2 | nn0addge1 | |- ( ( N e. RR /\ N e. NN0 ) -> N <_ ( N + N ) ) |
|
| 3 | 1 2 | mpancom | |- ( N e. NN0 -> N <_ ( N + N ) ) |
| 4 | nn0cn | |- ( N e. NN0 -> N e. CC ) |
|
| 5 | 4 | 2timesd | |- ( N e. NN0 -> ( 2 x. N ) = ( N + N ) ) |
| 6 | 3 5 | breqtrrd | |- ( N e. NN0 -> N <_ ( 2 x. N ) ) |