Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Glauco Siliprandi
Real intervals
ge0lere
Metamath Proof Explorer
Description: A nonnegative extended Real number smaller than or equal to a Real
number, is a Real number. (Contributed by Glauco Siliprandi , 24-Dec-2020)
Ref
Expression
Hypotheses
ge0lere.a
⊢ ( 𝜑 → 𝐴 ∈ ℝ )
ge0lere.b
⊢ ( 𝜑 → 𝐵 ∈ ( 0 [,] +∞ ) )
ge0lere.l
⊢ ( 𝜑 → 𝐵 ≤ 𝐴 )
Assertion
ge0lere
⊢ ( 𝜑 → 𝐵 ∈ ℝ )
Proof
Step
Hyp
Ref
Expression
1
ge0lere.a
⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2
ge0lere.b
⊢ ( 𝜑 → 𝐵 ∈ ( 0 [,] +∞ ) )
3
ge0lere.l
⊢ ( 𝜑 → 𝐵 ≤ 𝐴 )
4
iccssxr
⊢ ( 0 [,] +∞ ) ⊆ ℝ*
5
4 2
sseldi
⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
6
pnfxr
⊢ +∞ ∈ ℝ*
7
6
a1i
⊢ ( 𝜑 → +∞ ∈ ℝ* )
8
1
rexrd
⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
9
1
ltpnfd
⊢ ( 𝜑 → 𝐴 < +∞ )
10
5 8 7 3 9
xrlelttrd
⊢ ( 𝜑 → 𝐵 < +∞ )
11
5 7 10
xrltned
⊢ ( 𝜑 → 𝐵 ≠ +∞ )
12
ge0xrre
⊢ ( ( 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ≠ +∞ ) → 𝐵 ∈ ℝ )
13
2 11 12
syl2anc
⊢ ( 𝜑 → 𝐵 ∈ ℝ )