This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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