# Metamath Proof Explorer

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