Theorem xrge0nre

Description: An extended real which is not a real is plus infinity. (Contributed by Thierry Arnoux, 16-Oct-2017)

	Ref	Expression
Assertion	xrge0nre	$$⊢\left(A\in \left[0,\mathrm{+\infty }\right]\wedge \neg A\in ℝ\right)\to A=\mathrm{+\infty }$$

Proof

Step	Hyp	Ref	Expression
1		eliccxr	$$⊢A\in \left[0,\mathrm{+\infty }\right]\to A\in {ℝ}^{*}$$
2		xrge0neqmnf	$$⊢A\in \left[0,\mathrm{+\infty }\right]\to A\ne \mathrm{-\infty }$$
3		xrnemnf	$$⊢\left(A\in {ℝ}^{*}\wedge A\ne \mathrm{-\infty }\right)\leftrightarrow \left(A\in ℝ\vee A=\mathrm{+\infty }\right)$$
4	3	biimpi	$$⊢\left(A\in {ℝ}^{*}\wedge A\ne \mathrm{-\infty }\right)\to \left(A\in ℝ\vee A=\mathrm{+\infty }\right)$$
5	1 2 4	syl2anc	$$⊢A\in \left[0,\mathrm{+\infty }\right]\to \left(A\in ℝ\vee A=\mathrm{+\infty }\right)$$
6	5	orcanai	$$⊢\left(A\in \left[0,\mathrm{+\infty }\right]\wedge \neg A\in ℝ\right)\to A=\mathrm{+\infty }$$