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	$$⊢\phi \to A\in ℝ$$
	ge0lere.b	$$⊢\phi \to B\in \left[0,\mathrm{+\infty }\right]$$
	ge0lere.l	$$⊢\phi \to B\le A$$
Assertion	ge0lere	$$⊢\phi \to B\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		ge0lere.a	$$⊢\phi \to A\in ℝ$$
2		ge0lere.b	$$⊢\phi \to B\in \left[0,\mathrm{+\infty }\right]$$
3		ge0lere.l	$$⊢\phi \to B\le A$$
4		iccssxr	$$⊢\left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}$$
5	4 2	sselid	$$⊢\phi \to B\in {ℝ}^{*}$$
6		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
7	6	a1i	$$⊢\phi \to \mathrm{+\infty }\in {ℝ}^{*}$$
8	1	rexrd	$$⊢\phi \to A\in {ℝ}^{*}$$
9	1	ltpnfd	$$⊢\phi \to A<\mathrm{+\infty }$$
10	5 8 7 3 9	xrlelttrd	$$⊢\phi \to B<\mathrm{+\infty }$$
11	5 7 10	xrltned	$$⊢\phi \to B\ne \mathrm{+\infty }$$
12		ge0xrre	$$⊢\left(B\in \left[0,\mathrm{+\infty }\right]\wedge B\ne \mathrm{+\infty }\right)\to B\in ℝ$$
13	2 11 12	syl2anc	$$⊢\phi \to B\in ℝ$$