This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xrnpnfmnf

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

Step	Hyp	Ref	Expression
1		xrnpnfmnf.1	$⊢ φ \to A \in ℝ^{*}$
2		xrnpnfmnf.2	$⊢ φ \to \neg A \in ℝ$
3		xrnpnfmnf.3	$⊢ φ \to A \neq +∞$
4	1 3	jca	$⊢ φ \to (A \in ℝ^{*} \land A \neq +∞)$
5		xrnepnf	$⊢ (A \in ℝ^{*} \land A \neq +∞) \leftrightarrow (A \in ℝ \lor A = −∞)$
6	4 5	sylib	$⊢ φ \to (A \in ℝ \lor A = −∞)$
7		pm2.53	$⊢ (A \in ℝ \lor A = −∞) \to (\neg A \in ℝ \to A = −∞)$
8	6 2 7	sylc	$⊢ φ \to A = −∞$