xrre3

Description: A way of proving that an extended real is real. (Contributed by FL, 29-May-2014)

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

Step	Hyp	Ref	Expression
1		mnflt	$⊢ B \in ℝ \to −∞ < B$
2	1	adantl	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to −∞ < B$
3		mnfxr	$⊢ −∞ \in ℝ^{*}$
4		rexr	$⊢ B \in ℝ \to B \in ℝ^{*}$
5	4	adantl	$⊢ (A \in ℝ^{} \land B \in ℝ) \to B \in ℝ^{}$
6		simpl	$⊢ (A \in ℝ^{} \land B \in ℝ) \to A \in ℝ^{}$
7		xrltletr	$⊢ (−∞ \in ℝ^{} \land B \in ℝ^{} \land A \in ℝ^{*}) \to ((−∞ < B \land B \leq A) \to −∞ < A)$
8	3 5 6 7	mp3an2i	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to ((−∞ < B \land B \leq A) \to −∞ < A)$
9	2 8	mpand	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (B \leq A \to −∞ < A)$
10	9	imp	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land B \leq A) \to −∞ < A$
11	10	adantrr	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land (B \leq A \land A < +∞)) \to −∞ < A$
12		simprr	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land (B \leq A \land A < +∞)) \to A < +∞$
13		xrrebnd	$⊢ A \in ℝ^{*} \to (A \in ℝ \leftrightarrow (−∞ < A \land A < +∞))$
14	13	ad2antrr	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land (B \leq A \land A < +∞)) \to (A \in ℝ \leftrightarrow (−∞ < A \land A < +∞))$
15	11 12 14	mpbir2and	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land (B \leq A \land A < +∞)) \to A \in ℝ$

Metamath Proof Explorer