This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → 𝐵 ∈ ℝ )