xrnemnf

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

		Ref	Expression
	Assertion	xrnemnf	$⊢ (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	2 3	bitri	$⊢ A \in ℝ^{*} \leftrightarrow ((A \in ℝ \lor A = +∞) \lor A = −∞)$
5		df-ne	$⊢ A \neq −∞ \leftrightarrow \neg A = −∞$
6	4 5	anbi12i	$⊢ (A \in ℝ^{*} \land A \neq −∞) \leftrightarrow (((A \in ℝ \lor A = +∞) \lor A = −∞) \land \neg A = −∞)$
7		renemnf	$⊢ A \in ℝ \to A \neq −∞$
8		pnfnemnf	$⊢ +∞ \neq −∞$
9		neeq1	$⊢ A = +∞ \to (A \neq −∞ \leftrightarrow +∞ \neq −∞)$
10	8 9	mpbiri	$⊢ A = +∞ \to A \neq −∞$
11	7 10	jaoi	$⊢ (A \in ℝ \lor A = +∞) \to A \neq −∞$
12	11	neneqd	$⊢ (A \in ℝ \lor A = +∞) \to \neg A = −∞$
13	12	pm4.71i	$⊢ (A \in ℝ \lor A = +∞) \leftrightarrow ((A \in ℝ \lor A = +∞) \land \neg A = −∞)$
14	1 6 13	3bitr4i	$⊢ (A \in ℝ^{*} \land A \neq −∞) \leftrightarrow (A \in ℝ \lor A = +∞)$

Metamath Proof Explorer