# 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 ${⊢}\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{+\infty }\right)↔\left({A}\in ℝ\vee {A}=\mathrm{-\infty }\right)$

### Proof

Step Hyp Ref Expression
1 pm5.61 ${⊢}\left(\left(\left({A}\in ℝ\vee {A}=\mathrm{-\infty }\right)\vee {A}=\mathrm{+\infty }\right)\wedge ¬{A}=\mathrm{+\infty }\right)↔\left(\left({A}\in ℝ\vee {A}=\mathrm{-\infty }\right)\wedge ¬{A}=\mathrm{+\infty }\right)$
2 elxr ${⊢}{A}\in {ℝ}^{*}↔\left({A}\in ℝ\vee {A}=\mathrm{+\infty }\vee {A}=\mathrm{-\infty }\right)$
3 df-3or ${⊢}\left({A}\in ℝ\vee {A}=\mathrm{+\infty }\vee {A}=\mathrm{-\infty }\right)↔\left(\left({A}\in ℝ\vee {A}=\mathrm{+\infty }\right)\vee {A}=\mathrm{-\infty }\right)$
4 or32 ${⊢}\left(\left({A}\in ℝ\vee {A}=\mathrm{+\infty }\right)\vee {A}=\mathrm{-\infty }\right)↔\left(\left({A}\in ℝ\vee {A}=\mathrm{-\infty }\right)\vee {A}=\mathrm{+\infty }\right)$
5 2 3 4 3bitri ${⊢}{A}\in {ℝ}^{*}↔\left(\left({A}\in ℝ\vee {A}=\mathrm{-\infty }\right)\vee {A}=\mathrm{+\infty }\right)$
6 df-ne ${⊢}{A}\ne \mathrm{+\infty }↔¬{A}=\mathrm{+\infty }$
7 5 6 anbi12i ${⊢}\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{+\infty }\right)↔\left(\left(\left({A}\in ℝ\vee {A}=\mathrm{-\infty }\right)\vee {A}=\mathrm{+\infty }\right)\wedge ¬{A}=\mathrm{+\infty }\right)$
8 renepnf ${⊢}{A}\in ℝ\to {A}\ne \mathrm{+\infty }$
9 mnfnepnf ${⊢}\mathrm{-\infty }\ne \mathrm{+\infty }$
10 neeq1 ${⊢}{A}=\mathrm{-\infty }\to \left({A}\ne \mathrm{+\infty }↔\mathrm{-\infty }\ne \mathrm{+\infty }\right)$
11 9 10 mpbiri ${⊢}{A}=\mathrm{-\infty }\to {A}\ne \mathrm{+\infty }$
12 8 11 jaoi ${⊢}\left({A}\in ℝ\vee {A}=\mathrm{-\infty }\right)\to {A}\ne \mathrm{+\infty }$
13 12 neneqd ${⊢}\left({A}\in ℝ\vee {A}=\mathrm{-\infty }\right)\to ¬{A}=\mathrm{+\infty }$
14 13 pm4.71i ${⊢}\left({A}\in ℝ\vee {A}=\mathrm{-\infty }\right)↔\left(\left({A}\in ℝ\vee {A}=\mathrm{-\infty }\right)\wedge ¬{A}=\mathrm{+\infty }\right)$
15 1 7 14 3bitr4i ${⊢}\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{+\infty }\right)↔\left({A}\in ℝ\vee {A}=\mathrm{-\infty }\right)$