This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 \leq 2$

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