# 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
`|- ( ( A e. RR* /\ A =/= -oo ) <-> ( A e. RR \/ A = +oo ) )`

### Proof

Step Hyp Ref Expression
1 pm5.61
` |-  ( ( ( ( A e. RR \/ A = +oo ) \/ A = -oo ) /\ -. A = -oo ) <-> ( ( A e. RR \/ A = +oo ) /\ -. A = -oo ) )`
2 elxr
` |-  ( A e. RR* <-> ( A e. RR \/ A = +oo \/ A = -oo ) )`
3 df-3or
` |-  ( ( A e. RR \/ A = +oo \/ A = -oo ) <-> ( ( A e. RR \/ A = +oo ) \/ A = -oo ) )`
4 2 3 bitri
` |-  ( A e. RR* <-> ( ( A e. RR \/ A = +oo ) \/ A = -oo ) )`
5 df-ne
` |-  ( A =/= -oo <-> -. A = -oo )`
6 4 5 anbi12i
` |-  ( ( A e. RR* /\ A =/= -oo ) <-> ( ( ( A e. RR \/ A = +oo ) \/ A = -oo ) /\ -. A = -oo ) )`
7 renemnf
` |-  ( A e. RR -> A =/= -oo )`
8 pnfnemnf
` |-  +oo =/= -oo`
9 neeq1
` |-  ( A = +oo -> ( A =/= -oo <-> +oo =/= -oo ) )`
10 8 9 mpbiri
` |-  ( A = +oo -> A =/= -oo )`
11 7 10 jaoi
` |-  ( ( A e. RR \/ A = +oo ) -> A =/= -oo )`
12 11 neneqd
` |-  ( ( A e. RR \/ A = +oo ) -> -. A = -oo )`
13 12 pm4.71i
` |-  ( ( A e. RR \/ A = +oo ) <-> ( ( A e. RR \/ A = +oo ) /\ -. A = -oo ) )`
14 1 6 13 3bitr4i
` |-  ( ( A e. RR* /\ A =/= -oo ) <-> ( A e. RR \/ A = +oo ) )`