Theorem nn0lele2xi

Description: 'Less than or equal to' implies 'less than or equal to twice' for nonnegative integers. (Contributed by Raph Levien, 10-Dec-2002)

	Ref	Expression
Hypotheses	nn0lele2xi.1	|- M e. NN0
	nn0lele2xi.2	|- N e. NN0
Assertion	nn0lele2xi	|- ( N <_ M -> N <_ ( 2 x. M ) )

Proof

Step	Hyp	Ref	Expression
1		nn0lele2xi.1	|- M e. NN0
2		nn0lele2xi.2	|- N e. NN0
3	1	nn0le2xi	|- M <_ ( 2 x. M )
4	2	nn0rei	|- N e. RR
5	1	nn0rei	|- M e. RR
6		2re	|- 2 e. RR
7	6 5	remulcli	|- ( 2 x. M ) e. RR
8	4 5 7	letri	|- ( ( N <_ M /\ M <_ ( 2 x. M ) ) -> N <_ ( 2 x. M ) )
9	3 8	mpan2	|- ( N <_ M -> N <_ ( 2 x. M ) )