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