Metamath Proof Explorer


Theorem nn0le2xi

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 )

Proof

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 )