Metamath Proof Explorer

Theorem xrre2

Description: An extended real between two others is real. (Contributed by NM, 6-Feb-2007)

		Ref	Expression
	Assertion	xrre2	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A < B \land B < C)) \to B \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		mnfle	$⊢ A \in ℝ^{*} \to −∞ \leq A$
2	1	adantr	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to −∞ \leq A$
3		mnfxr	$⊢ −∞ \in ℝ^{*}$
4		xrlelttr	$⊢ (−∞ \in ℝ^{} \land A \in ℝ^{} \land B \in ℝ^{*}) \to ((−∞ \leq A \land A < B) \to −∞ < B)$
5	3 4	mp3an1	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((−∞ \leq A \land A < B) \to −∞ < B)$
6	2 5	mpand	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A < B \to −∞ < B)$
7	6	3adant3	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to (A < B \to −∞ < B)$
8		pnfge	$⊢ C \in ℝ^{*} \to C \leq +∞$
9	8	adantl	$⊢ (B \in ℝ^{} \land C \in ℝ^{}) \to C \leq +∞$
10		pnfxr	$⊢ +∞ \in ℝ^{*}$
11		xrltletr	$⊢ (B \in ℝ^{} \land C \in ℝ^{} \land +∞ \in ℝ^{*}) \to ((B < C \land C \leq +∞) \to B < +∞)$
12	10 11	mp3an3	$⊢ (B \in ℝ^{} \land C \in ℝ^{}) \to ((B < C \land C \leq +∞) \to B < +∞)$
13	9 12	mpan2d	$⊢ (B \in ℝ^{} \land C \in ℝ^{}) \to (B < C \to B < +∞)$
14	13	3adant1	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to (B < C \to B < +∞)$
15	7 14	anim12d	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to ((A < B \land B < C) \to (−∞ < B \land B < +∞))$
16		xrrebnd	$⊢ B \in ℝ^{*} \to (B \in ℝ \leftrightarrow (−∞ < B \land B < +∞))$
17	16	3ad2ant2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to (B \in ℝ \leftrightarrow (−∞ < B \land B < +∞))$
18	15 17	sylibrd	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to ((A < B \land B < C) \to B \in ℝ)$
19	18	imp	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A < B \land B < C)) \to B \in ℝ$