Theorem nn0le2xi

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

	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	1	nn0rei	$$⊢N\in ℝ$$
3	2 1	nn0addge1i	$$⊢N\le N+N$$
4	1	nn0cni	$$⊢N\in ℂ$$
5	4	2timesi	$$⊢2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=N+N$$
6	3 5	breqtrri	$$⊢N\le 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$