This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ( 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 or32 
 |-  ( ( ( A e. RR \/ A = +oo ) \/ A = -oo ) <-> ( ( A e. RR \/ A = -oo ) \/ A = +oo ) )
5 2 3 4 3bitri 
 |-  ( A e. RR* <-> ( ( A e. RR \/ A = -oo ) \/ A = +oo ) )
6 df-ne 
 |-  ( A =/= +oo <-> -. A = +oo )
7 5 6 anbi12i 
 |-  ( ( A e. RR* /\ A =/= +oo ) <-> ( ( ( A e. RR \/ A = -oo ) \/ A = +oo ) /\ -. A = +oo ) )
8 renepnf 
 |-  ( A e. RR -> A =/= +oo )
9 mnfnepnf 
 |-  -oo =/= +oo
10 neeq1 
 |-  ( A = -oo -> ( A =/= +oo <-> -oo =/= +oo ) )
11 9 10 mpbiri 
 |-  ( A = -oo -> A =/= +oo )
12 8 11 jaoi 
 |-  ( ( A e. RR \/ A = -oo ) -> A =/= +oo )
13 12 neneqd 
 |-  ( ( A e. RR \/ A = -oo ) -> -. A = +oo )
14 13 pm4.71i 
 |-  ( ( A e. RR \/ A = -oo ) <-> ( ( A e. RR \/ A = -oo ) /\ -. A = +oo ) )
15 1 7 14 3bitr4i 
 |-  ( ( A e. RR* /\ A =/= +oo ) <-> ( A e. RR \/ A = -oo ) )