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 ) )