Metamath Proof Explorer


Theorem xrrege0

Description: A nonnegative extended real that is less than a real bound is real. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xrrege0 ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) → 𝐴 ∈ ℝ )

Proof

Step Hyp Ref Expression
1 ge0gtmnf ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) → -∞ < 𝐴 )
2 1 ad2ant2r ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) → -∞ < 𝐴 )
3 simprr ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) → 𝐴𝐵 )
4 2 3 jca ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) → ( -∞ < 𝐴𝐴𝐵 ) )
5 xrre ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ ) ∧ ( -∞ < 𝐴𝐴𝐵 ) ) → 𝐴 ∈ ℝ )
6 4 5 syldan ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴𝐴𝐵 ) ) → 𝐴 ∈ ℝ )