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\in {\mathbb{N}}_0$$
	nn0lele2xi.2	$$⊢N\in {\mathbb{N}}_0$$
Assertion	nn0lele2xi	$$⊢N\le M\to N\le 2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$

Proof

Step	Hyp	Ref	Expression
1		nn0lele2xi.1	$$⊢M\in {\mathbb{N}}_0$$
2		nn0lele2xi.2	$$⊢N\in {\mathbb{N}}_0$$
3	1	nn0le2xi	$$⊢M\le 2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
4	2	nn0rei	$$⊢N\in ℝ$$
5	1	nn0rei	$$⊢M\in ℝ$$
6		2re	$$⊢2\in ℝ$$
7	6 5	remulcli	$$⊢2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\in ℝ$$
8	4 5 7	letri	$$⊢\left(N\le M\wedge M\le 2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\right)\to N\le 2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
9	3 8	mpan2	$$⊢N\le M\to N\le 2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$