xrrege0

Description: A nonnegative extended real that is less than a real bound is real. (Contributed by Mario Carneiro, 20-Aug-2015)

		Ref	Expression
	Assertion	xrrege0	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land (0 \leq A \land A \leq B)) \to A \in ℝ$

Step	Hyp	Ref	Expression
1		ge0gtmnf	$⊢ (A \in ℝ^{*} \land 0 \leq A) \to −∞ < A$
2	1	ad2ant2r	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land (0 \leq A \land A \leq B)) \to −∞ < A$
3		simprr	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land (0 \leq A \land A \leq B)) \to A \leq B$
4	2 3	jca	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land (0 \leq A \land A \leq B)) \to (−∞ < A \land A \leq B)$
5		xrre	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land (−∞ < A \land A \leq B)) \to A \in ℝ$
6	4 5	syldan	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land (0 \leq A \land A \leq B)) \to A \in ℝ$

Metamath Proof Explorer