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

Metamath Proof Explorer

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