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	|- ( ph -> A e. RR )
	ge0lere.b	|- ( ph -> B e. ( 0 [,] +oo ) )
	ge0lere.l	|- ( ph -> B <_ A )
Assertion	ge0lere	|- ( ph -> B e. RR )

Proof

Step	Hyp	Ref	Expression
1		ge0lere.a	|- ( ph -> A e. RR )
2		ge0lere.b	|- ( ph -> B e. ( 0 [,] +oo ) )
3		ge0lere.l	|- ( ph -> B <_ A )
4		iccssxr	|- ( 0 [,] +oo ) C_ RR*
5	4 2	sseldi	|- ( ph -> B e. RR* )
6		pnfxr	|- +oo e. RR*
7	6	a1i	|- ( ph -> +oo e. RR* )
8	1	rexrd	|- ( ph -> A e. RR* )
9	1	ltpnfd	|- ( ph -> A < +oo )
10	5 8 7 3 9	xrlelttrd	|- ( ph -> B < +oo )
11	5 7 10	xrltned	|- ( ph -> B =/= +oo )
12		ge0xrre	|- ( ( B e. ( 0 [,] +oo ) /\ B =/= +oo ) -> B e. RR )
13	2 11 12	syl2anc	|- ( ph -> B e. RR )