Theorem xrnpnfmnf

Description: An extended real that is neither real nor plus infinity, is minus infinity. (Contributed by Glauco Siliprandi, 5-Feb-2022)

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

Proof

Step	Hyp	Ref	Expression
1		xrnpnfmnf.1	$$⊢\phi \to A\in {ℝ}^{*}$$
2		xrnpnfmnf.2	$$⊢\phi \to \neg A\in ℝ$$
3		xrnpnfmnf.3	$$⊢\phi \to A\ne \mathrm{+\infty }$$
4	1 3	jca	$$⊢\phi \to \left(A\in {ℝ}^{*}\wedge A\ne \mathrm{+\infty }\right)$$
5		xrnepnf	$$⊢\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 }$$