Theorem rpgecl

Description: A number greater than or equal to a positive real is positive real. (Contributed by Mario Carneiro, 28-May-2016)

	Ref	Expression
Assertion	rpgecl	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℝ\wedge A\le B\right)\to B\in {ℝ}^{+}$$

Proof

Step	Hyp	Ref	Expression
1		simp2	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℝ\wedge A\le B\right)\to B\in ℝ$$
2		0red	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℝ\wedge A\le B\right)\to 0\in ℝ$$
3		rpre	$$⊢A\in {ℝ}^{+}\to A\in ℝ$$
4	3	3ad2ant1	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℝ\wedge A\le B\right)\to A\in ℝ$$
5		rpgt0	$$⊢A\in {ℝ}^{+}\to 0<A$$
6	5	3ad2ant1	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℝ\wedge A\le B\right)\to 0<A$$
7		simp3	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℝ\wedge A\le B\right)\to A\le B$$
8	2 4 1 6 7	ltletrd	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℝ\wedge A\le B\right)\to 0<B$$
9		elrp	$$⊢B\in {ℝ}^{+}\leftrightarrow \left(B\in ℝ\wedge 0<B\right)$$
10	1 8 9	sylanbrc	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℝ\wedge A\le B\right)\to B\in {ℝ}^{+}$$