Theorem xrred

Description: An extended real that is neither minus infinity, nor plus infinity, is real. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	xrred.1	$$⊢\phi \to A\in {ℝ}^{*}$$
	xrred.2	$$⊢\phi \to A\ne \mathrm{-\infty }$$
	xrred.3	$$⊢\phi \to A\ne \mathrm{+\infty }$$
Assertion	xrred	$$⊢\phi \to A\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		xrred.1	$$⊢\phi \to A\in {ℝ}^{*}$$
2		xrred.2	$$⊢\phi \to A\ne \mathrm{-\infty }$$
3		xrred.3	$$⊢\phi \to A\ne \mathrm{+\infty }$$
4	1 2	jca	$$⊢\phi \to \left(A\in {ℝ}^{*}\wedge A\ne \mathrm{-\infty }\right)$$
5		xrnemnf	$$⊢\left(A\in {ℝ}^{*}\wedge A\ne \mathrm{-\infty }\right)\leftrightarrow \left(A\in ℝ\vee A=\mathrm{+\infty }\right)$$
6	4 5	sylib	$$⊢\phi \to \left(A\in ℝ\vee A=\mathrm{+\infty }\right)$$
7	3	neneqd	$$⊢\phi \to \neg A=\mathrm{+\infty }$$
8		pm2.53	$$⊢\left(A\in ℝ\vee A=\mathrm{+\infty }\right)\to \left(\neg A\in ℝ\to A=\mathrm{+\infty }\right)$$
9	8	con1d	$$⊢\left(A\in ℝ\vee A=\mathrm{+\infty }\right)\to \left(\neg A=\mathrm{+\infty }\to A\in ℝ\right)$$
10	6 7 9	sylc	$$⊢\phi \to A\in ℝ$$