Theorem 0le2

Description: The number 0 is less than or equal to 2. (Contributed by David A. Wheeler, 7-Dec-2018)

	Ref	Expression
Assertion	0le2	$$⊢0\le 2$$

Proof

Step	Hyp	Ref	Expression
1		0le1	$$⊢0\le 1$$
2		1re	$$⊢1\in ℝ$$
3	2 2	addge0i	$$⊢\left(0\le 1\wedge 0\le 1\right)\to 0\le 1+1$$
4	1 1 3	mp2an	$$⊢0\le 1+1$$
5		df-2	$$⊢2=1+1$$
6	4 5	breqtrri	$$⊢0\le 2$$