xrnepnf

Description: An extended real other than plus infinity is real or negative infinite. (Contributed by Mario Carneiro, 20-Aug-2015)

		Ref	Expression
	Assertion	xrnepnf	$⊢ (A \in ℝ^{*} \land A \neq +∞) \leftrightarrow (A \in ℝ \lor A = −∞)$

Step	Hyp	Ref	Expression
1		pm5.61	$⊢ (((A \in ℝ \lor A = −∞) \lor A = +∞) \land \neg A = +∞) \leftrightarrow ((A \in ℝ \lor A = −∞) \land \neg A = +∞)$
2		elxr	$⊢ A \in ℝ^{*} \leftrightarrow (A \in ℝ \lor A = +∞ \lor A = −∞)$
3		df-3or	$⊢ (A \in ℝ \lor A = +∞ \lor A = −∞) \leftrightarrow ((A \in ℝ \lor A = +∞) \lor A = −∞)$
4		or32	$⊢ ((A \in ℝ \lor A = +∞) \lor A = −∞) \leftrightarrow ((A \in ℝ \lor A = −∞) \lor A = +∞)$
5	2 3 4	3bitri	$⊢ A \in ℝ^{*} \leftrightarrow ((A \in ℝ \lor A = −∞) \lor A = +∞)$
6		df-ne	$⊢ A \neq +∞ \leftrightarrow \neg A = +∞$
7	5 6	anbi12i	$⊢ (A \in ℝ^{*} \land A \neq +∞) \leftrightarrow (((A \in ℝ \lor A = −∞) \lor A = +∞) \land \neg A = +∞)$
8		renepnf	$⊢ A \in ℝ \to A \neq +∞$
9		mnfnepnf	$⊢ −∞ \neq +∞$
10		neeq1	$⊢ A = −∞ \to (A \neq +∞ \leftrightarrow −∞ \neq +∞)$
11	9 10	mpbiri	$⊢ A = −∞ \to A \neq +∞$
12	8 11	jaoi	$⊢ (A \in ℝ \lor A = −∞) \to A \neq +∞$
13	12	neneqd	$⊢ (A \in ℝ \lor A = −∞) \to \neg A = +∞$
14	13	pm4.71i	$⊢ (A \in ℝ \lor A = −∞) \leftrightarrow ((A \in ℝ \lor A = −∞) \land \neg A = +∞)$
15	1 7 14	3bitr4i	$⊢ (A \in ℝ^{*} \land A \neq +∞) \leftrightarrow (A \in ℝ \lor A = −∞)$

Metamath Proof Explorer