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 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵 ) ) → 𝐴 ∈ ℝ )