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