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 ⊢ M ∈ ℕ 0
nn0lele2xi.2 ⊢ N ∈ ℕ 0
Assertion nn0lele2xi ⊢ N ≤ M → N ≤ 2 ⋅ M

Proof

Step Hyp Ref Expression
1 nn0lele2xi.1 ⊢ M ∈ ℕ 0
2 nn0lele2xi.2 ⊢ N ∈ ℕ 0
3 1 nn0le2xi ⊢ M ≤ 2 ⋅ M
4 2 nn0rei ⊢ N ∈ ℝ
5 1 nn0rei ⊢ M ∈ ℝ
6 2re ⊢ 2 ∈ ℝ
7 6 5 remulcli ⊢ 2 ⋅ M ∈ ℝ
8 4 5 7 letri ⊢ N ≤ M ∧ M ≤ 2 ⋅ M → N ≤ 2 ⋅ M
9 3 8 mpan2 ⊢ N ≤ M → N ≤ 2 ⋅ M