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