This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 · 𝑀 ) )