Theorem 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	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) ↔ ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		pm5.61	⊢ ( ( ( ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ) ∨ 𝐴 = -∞ ) ∧ ¬ 𝐴 = -∞ ) ↔ ( ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ) ∧ ¬ 𝐴 = -∞ ) )
2		elxr	⊢ ( 𝐴 ∈ ℝ* ↔ ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) )
3		df-3or	⊢ ( ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) ↔ ( ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ) ∨ 𝐴 = -∞ ) )
4	2 3	bitri	⊢ ( 𝐴 ∈ ℝ* ↔ ( ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ) ∨ 𝐴 = -∞ ) )
5		df-ne	⊢ ( 𝐴 ≠ -∞ ↔ ¬ 𝐴 = -∞ )
6	4 5	anbi12i	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) ↔ ( ( ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ) ∨ 𝐴 = -∞ ) ∧ ¬ 𝐴 = -∞ ) )
7		renemnf	⊢ ( 𝐴 ∈ ℝ → 𝐴 ≠ -∞ )
8		pnfnemnf	⊢ +∞ ≠ -∞
9		neeq1	⊢ ( 𝐴 = +∞ → ( 𝐴 ≠ -∞ ↔ +∞ ≠ -∞ ) )
10	8 9	mpbiri	⊢ ( 𝐴 = +∞ → 𝐴 ≠ -∞ )
11	7 10	jaoi	⊢ ( ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ) → 𝐴 ≠ -∞ )
12	11	neneqd	⊢ ( ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ) → ¬ 𝐴 = -∞ )
13	12	pm4.71i	⊢ ( ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ) ↔ ( ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ) ∧ ¬ 𝐴 = -∞ ) )
14	1 6 13	3bitr4i	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) ↔ ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ) )