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 φ A
ge0lere.b φ B 0 +∞
ge0lere.l φ B A
Assertion ge0lere φ B

Proof

Step Hyp Ref Expression
1 ge0lere.a φ A
2 ge0lere.b φ B 0 +∞
3 ge0lere.l φ B A
4 iccssxr 0 +∞ *
5 4 2 sseldi φ B *
6 pnfxr +∞ *
7 6 a1i φ +∞ *
8 1 rexrd φ A *
9 1 ltpnfd φ A < +∞
10 5 8 7 3 9 xrlelttrd φ B < +∞
11 5 7 10 xrltned φ B +∞
12 ge0xrre B 0 +∞ B +∞ B
13 2 11 12 syl2anc φ B