Theorem rpge0

Description: A positive real is greater than or equal to zero. (Contributed by NM, 22-Feb-2008)

	Ref	Expression
Assertion	rpge0	$$⊢A\in {ℝ}^{+}\to 0\le A$$

Proof

Step	Hyp	Ref	Expression
1		rpre	$$⊢A\in {ℝ}^{+}\to A\in ℝ$$
2		rpgt0	$$⊢A\in {ℝ}^{+}\to 0<A$$
3		0re	$$⊢0\in ℝ$$
4		ltle	$$⊢\left(0\in ℝ\wedge A\in ℝ\right)\to \left(0<A\to 0\le A\right)$$
5	3 4	mpan	$$⊢A\in ℝ\to \left(0<A\to 0\le A\right)$$
6	1 2 5	sylc	$$⊢A\in {ℝ}^{+}\to 0\le A$$