# 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 ${⊢}\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 2 3 bitri ${⊢}{A}\in {ℝ}^{*}↔\left(\left({A}\in ℝ\vee {A}=\mathrm{+\infty }\right)\vee {A}=\mathrm{-\infty }\right)$
5 df-ne ${⊢}{A}\ne \mathrm{-\infty }↔¬{A}=\mathrm{-\infty }$
6 4 5 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)$
7 renemnf ${⊢}{A}\in ℝ\to {A}\ne \mathrm{-\infty }$
8 pnfnemnf ${⊢}\mathrm{+\infty }\ne \mathrm{-\infty }$
9 neeq1 ${⊢}{A}=\mathrm{+\infty }\to \left({A}\ne \mathrm{-\infty }↔\mathrm{+\infty }\ne \mathrm{-\infty }\right)$
10 8 9 mpbiri ${⊢}{A}=\mathrm{+\infty }\to {A}\ne \mathrm{-\infty }$
11 7 10 jaoi ${⊢}\left({A}\in ℝ\vee {A}=\mathrm{+\infty }\right)\to {A}\ne \mathrm{-\infty }$
12 11 neneqd ${⊢}\left({A}\in ℝ\vee {A}=\mathrm{+\infty }\right)\to ¬{A}=\mathrm{-\infty }$
13 12 pm4.71i ${⊢}\left({A}\in ℝ\vee {A}=\mathrm{+\infty }\right)↔\left(\left({A}\in ℝ\vee {A}=\mathrm{+\infty }\right)\wedge ¬{A}=\mathrm{-\infty }\right)$
14 1 6 13 3bitr4i ${⊢}\left({A}\in {ℝ}^{*}\wedge {A}\ne \mathrm{-\infty }\right)↔\left({A}\in ℝ\vee {A}=\mathrm{+\infty }\right)$