Theorem nn0le2x

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

	Ref	Expression
Assertion	nn0le2x	$$⊢N\in {\mathbb{N}}_0\to N\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$

Proof

Step	Hyp	Ref	Expression
1		nn0re	$$⊢N\in {\mathbb{N}}_0\to N\in ℝ$$
2		nn0addge1	$$⊢\left(N\in ℝ\wedge N\in {\mathbb{N}}_0\right)\to N\le N+N$$
3	1 2	mpancom	$$⊢N\in {\mathbb{N}}_0\to N\le N+N$$
4		nn0cn	$$⊢N\in {\mathbb{N}}_0\to N\in ℂ$$
5	4	2timesd	$$⊢N\in {\mathbb{N}}_0\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=N+N$$
6	3 5	breqtrrd	$$⊢N\in {\mathbb{N}}_0\to N\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$