Metamath Proof Explorer

Theorem nn0le2xi

Description: A nonnegative integer is less than or equal to twice itself. (Contributed by Raph Levien, 10-Dec-2002)

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 1 nn0rei 
 |-  N e. RR
3 2 1 nn0addge1i 
 |-  N <_ ( N + N )
4 1 nn0cni 
 |-  N e. CC
5 4 2timesi 
 |-  ( 2 x. N ) = ( N + N )
6 3 5 breqtrri 
 |-  N <_ ( 2 x. N )