Metamath Proof Explorer


Theorem nn0le2xi

Description: A nonnegative integer is less than or equal to twice itself. (Contributed by Raph Levien, 10-Dec-2002) (Proof shortened by AV, 9-Sep-2025)

Ref Expression
Hypothesis nn0le2xi.1 𝑁 ∈ ℕ0
Assertion nn0le2xi 𝑁 ≤ ( 2 · 𝑁 )

Proof

Step Hyp Ref Expression
1 nn0le2xi.1 𝑁 ∈ ℕ0
2 nn0le2x ( 𝑁 ∈ ℕ0𝑁 ≤ ( 2 · 𝑁 ) )
3 1 2 ax-mp 𝑁 ≤ ( 2 · 𝑁 )