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	$⊢ (A \in ℝ^{+} \land B \in ℝ \land A \leq B) \to B \in ℝ^{+}$

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

Metamath Proof Explorer