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	⊢ 𝑀 ∈ ℕ0
	nn0lele2xi.2	⊢ 𝑁 ∈ ℕ0
Assertion	nn0lele2xi	⊢ ( 𝑁 ≤ 𝑀 → 𝑁 ≤ ( 2 · 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		nn0lele2xi.1	⊢ 𝑀 ∈ ℕ0
2		nn0lele2xi.2	⊢ 𝑁 ∈ ℕ0
3	1	nn0le2xi	⊢ 𝑀 ≤ ( 2 · 𝑀 )
4	2	nn0rei	⊢ 𝑁 ∈ ℝ
5	1	nn0rei	⊢ 𝑀 ∈ ℝ
6		2re	⊢ 2 ∈ ℝ
7	6 5	remulcli	⊢ ( 2 · 𝑀 ) ∈ ℝ
8	4 5 7	letri	⊢ ( ( 𝑁 ≤ 𝑀 ∧ 𝑀 ≤ ( 2 · 𝑀 ) ) → 𝑁 ≤ ( 2 · 𝑀 ) )
9	3 8	mpan2	⊢ ( 𝑁 ≤ 𝑀 → 𝑁 ≤ ( 2 · 𝑀 ) )