Theorem xrre2

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

	Ref	Expression
Assertion	xrre2	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → 𝐵 ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		mnfle	⊢ ( 𝐴 ∈ ℝ* → -∞ ≤ 𝐴 )
2	1	adantr	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → -∞ ≤ 𝐴 )
3		mnfxr	⊢ -∞ ∈ ℝ*
4		xrlelttr	⊢ ( ( -∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( -∞ ≤ 𝐴 ∧ 𝐴 < 𝐵 ) → -∞ < 𝐵 ) )
5	3 4	mp3an1	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( -∞ ≤ 𝐴 ∧ 𝐴 < 𝐵 ) → -∞ < 𝐵 ) )
6	2 5	mpand	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 → -∞ < 𝐵 ) )
7	6	3adant3	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝐴 < 𝐵 → -∞ < 𝐵 ) )
8		pnfge	⊢ ( 𝐶 ∈ ℝ* → 𝐶 ≤ +∞ )
9	8	adantl	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → 𝐶 ≤ +∞ )
10		pnfxr	⊢ +∞ ∈ ℝ*
11		xrltletr	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( 𝐵 < 𝐶 ∧ 𝐶 ≤ +∞ ) → 𝐵 < +∞ ) )
12	10 11	mp3an3	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ( 𝐵 < 𝐶 ∧ 𝐶 ≤ +∞ ) → 𝐵 < +∞ ) )
13	9 12	mpan2d	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝐵 < 𝐶 → 𝐵 < +∞ ) )
14	13	3adant1	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝐵 < 𝐶 → 𝐵 < +∞ ) )
15	7 14	anim12d	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → ( -∞ < 𝐵 ∧ 𝐵 < +∞ ) ) )
16		xrrebnd	⊢ ( 𝐵 ∈ ℝ* → ( 𝐵 ∈ ℝ ↔ ( -∞ < 𝐵 ∧ 𝐵 < +∞ ) ) )
17	16	3ad2ant2	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝐵 ∈ ℝ ↔ ( -∞ < 𝐵 ∧ 𝐵 < +∞ ) ) )
18	15 17	sylibrd	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → 𝐵 ∈ ℝ ) )
19	18	imp	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → 𝐵 ∈ ℝ )