Theorem xrge0neqmnf

Description: A nonnegative extended real is not equal to minus infinity. (Contributed by Thierry Arnoux, 9-Jun-2017) (Proof shortened by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	xrge0neqmnf	$$⊢A\in \left[0,\mathrm{+\infty }\right]\to A\ne \mathrm{-\infty }$$

Proof

Step	Hyp	Ref	Expression
1		eliccxr	$$⊢A\in \left[0,\mathrm{+\infty }\right]\to A\in {ℝ}^{*}$$
2		0xr	$$⊢0\in {ℝ}^{*}$$
3		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
4		iccgelb	$$⊢\left(0\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\wedge A\in \left[0,\mathrm{+\infty }\right]\right)\to 0\le A$$
5	2 3 4	mp3an12	$$⊢A\in \left[0,\mathrm{+\infty }\right]\to 0\le A$$
6		ge0nemnf	$$⊢\left(A\in {ℝ}^{*}\wedge 0\le A\right)\to A\ne \mathrm{-\infty }$$
7	1 5 6	syl2anc	$$⊢A\in \left[0,\mathrm{+\infty }\right]\to A\ne \mathrm{-\infty }$$