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	$$⊢N\in {\mathbb{N}}_0$$
Assertion	nn0le2xi	$$⊢N\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$

Proof

Step	Hyp	Ref	Expression
1		nn0le2xi.1	$$⊢N\in {\mathbb{N}}_0$$
2		nn0le2x	$$⊢N\in {\mathbb{N}}_0\to N\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
3	1 2	ax-mp	$$⊢N\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$