Theorem xrge0nemnfd

Description: A nonnegative extended real is not minus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypothesis	xrge0nemnfd.1	$$⊢\phi \to A\in \left[0,\mathrm{+\infty }\right]$$
Assertion	xrge0nemnfd	$$⊢\phi \to A\ne \mathrm{-\infty }$$

Proof

Step	Hyp	Ref	Expression
1		xrge0nemnfd.1	$$⊢\phi \to A\in \left[0,\mathrm{+\infty }\right]$$
2		mnfxr	$$⊢\mathrm{-\infty }\in {ℝ}^{*}$$
3	2	a1i	$$⊢\phi \to \mathrm{-\infty }\in {ℝ}^{*}$$
4		iccssxr	$$⊢\left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}$$
5	4 1	sselid	$$⊢\phi \to A\in {ℝ}^{*}$$
6		0xr	$$⊢0\in {ℝ}^{*}$$
7	6	a1i	$$⊢\phi \to 0\in {ℝ}^{*}$$
8		mnflt0	$$⊢\mathrm{-\infty }<0$$
9	8	a1i	$$⊢\phi \to \mathrm{-\infty }<0$$
10		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
11	10	a1i	$$⊢\phi \to \mathrm{+\infty }\in {ℝ}^{*}$$
12		iccgelb	$$⊢\left(0\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\wedge A\in \left[0,\mathrm{+\infty }\right]\right)\to 0\le A$$
13	7 11 1 12	syl3anc	$$⊢\phi \to 0\le A$$
14	3 7 5 9 13	xrltletrd	$$⊢\phi \to \mathrm{-\infty }<A$$
15	3 5 14	xrgtned	$$⊢\phi \to A\ne \mathrm{-\infty }$$