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