Metamath Proof Explorer


Theorem ge0lere

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 ( 𝜑𝐵 ∈ ℝ )