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

Proof

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