xrred

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

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

Metamath Proof Explorer