Theorem xrnmnfpnf

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

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

Proof

Step	Hyp	Ref	Expression
1		xrnmnfpnf.1	$$⊢\phi \to A\in {ℝ}^{*}$$
2		xrnmnfpnf.2	$$⊢\phi \to \neg A\in ℝ$$
3		xrnmnfpnf.3	$$⊢\phi \to A\ne \mathrm{-\infty }$$
4	1 3	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		pm2.53	$$⊢\left(A\in ℝ\vee A=\mathrm{+\infty }\right)\to \left(\neg A\in ℝ\to A=\mathrm{+\infty }\right)$$
8	6 2 7	sylc	$$⊢\phi \to A=\mathrm{+\infty }$$