xrre

Description: A way of proving that an extended real is real. (Contributed by NM, 9-Mar-2006)

		Ref	Expression
	Assertion	xrre	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land (−∞ < A \land A \leq B)) \to A \in ℝ$

Step	Hyp	Ref	Expression
1		simprl	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land (−∞ < A \land A \leq B)) \to −∞ < A$
2		ltpnf	$⊢ B \in ℝ \to B < +∞$
3	2	adantl	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to B < +∞$
4		rexr	$⊢ B \in ℝ \to B \in ℝ^{*}$
5		pnfxr	$⊢ +∞ \in ℝ^{*}$
6		xrlelttr	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land +∞ \in ℝ^{*}) \to ((A \leq B \land B < +∞) \to A < +∞)$
7	5 6	mp3an3	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((A \leq B \land B < +∞) \to A < +∞)$
8	4 7	sylan2	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to ((A \leq B \land B < +∞) \to A < +∞)$
9	3 8	mpan2d	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (A \leq B \to A < +∞)$
10	9	imp	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land A \leq B) \to A < +∞$
11	10	adantrl	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land (−∞ < A \land A \leq B)) \to A < +∞$
12		xrrebnd	$⊢ A \in ℝ^{*} \to (A \in ℝ \leftrightarrow (−∞ < A \land A < +∞))$
13	12	ad2antrr	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land (−∞ < A \land A \leq B)) \to (A \in ℝ \leftrightarrow (−∞ < A \land A < +∞))$
14	1 11 13	mpbir2and	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land (−∞ < A \land A \leq B)) \to A \in ℝ$

Metamath Proof Explorer