Theorem 0le2OLD

Description: Obsolete version of 0le2 as of 10-Jun-2026. (Contributed by David A. Wheeler, 7-Dec-2018) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	0le2OLD	$$⊢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$$