Metamath Proof Explorer

Theorem xrre3

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

Ref Expression
Assertion xrre3 ⊢ A ∈ ℝ * ∧ B ∈ ℝ ∧ B ≤ A ∧ A < +∞ → A ∈ ℝ

Proof

Step Hyp Ref Expression
1 mnflt ⊢ B ∈ ℝ → −∞ < B
2 1 adantl ⊢ A ∈ ℝ * ∧ B ∈ ℝ → −∞ < B
3 mnfxr ⊢ −∞ ∈ ℝ *
4 rexr ⊢ B ∈ ℝ → B ∈ ℝ *
5 4 adantl ⊢ A ∈ ℝ * ∧ B ∈ ℝ → B ∈ ℝ *
6 simpl ⊢ A ∈ ℝ * ∧ B ∈ ℝ → A ∈ ℝ *
7 xrltletr ⊢ −∞ ∈ ℝ * ∧ B ∈ ℝ * ∧ A ∈ ℝ * → −∞ < B ∧ B ≤ A → −∞ < A
8 3 5 6 7 mp3an2i ⊢ A ∈ ℝ * ∧ B ∈ ℝ → −∞ < B ∧ B ≤ A → −∞ < A
9 2 8 mpand ⊢ A ∈ ℝ * ∧ B ∈ ℝ → B ≤ A → −∞ < A
10 9 imp ⊢ A ∈ ℝ * ∧ B ∈ ℝ ∧ B ≤ A → −∞ < A
11 10 adantrr ⊢ A ∈ ℝ * ∧ B ∈ ℝ ∧ B ≤ A ∧ A < +∞ → −∞ < A
12 simprr ⊢ A ∈ ℝ * ∧ B ∈ ℝ ∧ B ≤ A ∧ A < +∞ → A < +∞
13 xrrebnd ⊢ A ∈ ℝ * → A ∈ ℝ ↔ −∞ < A ∧ A < +∞
14 13 ad2antrr ⊢ A ∈ ℝ * ∧ B ∈ ℝ ∧ B ≤ A ∧ A < +∞ → A ∈ ℝ ↔ −∞ < A ∧ A < +∞
15 11 12 14 mpbir2and ⊢ A ∈ ℝ * ∧ B ∈ ℝ ∧ B ≤ A ∧ A < +∞ → A ∈ ℝ