Theorem xrge0nre

Description: An extended real which is not a real is plus infinity. (Contributed by Thierry Arnoux, 16-Oct-2017)

	Ref	Expression
Assertion	xrge0nre	|- ( ( A e. ( 0 [,] +oo ) /\ -. A e. RR ) -> A = +oo )

Proof

Step	Hyp	Ref	Expression
1		eliccxr	|- ( A e. ( 0 [,] +oo ) -> A e. RR* )
2		xrge0neqmnf	|- ( A e. ( 0 [,] +oo ) -> A =/= -oo )
3		xrnemnf	|- ( ( A e. RR* /\ A =/= -oo ) <-> ( A e. RR \/ A = +oo ) )
4	3	biimpi	|- ( ( A e. RR* /\ A =/= -oo ) -> ( A e. RR \/ A = +oo ) )
5	1 2 4	syl2anc	|- ( A e. ( 0 [,] +oo ) -> ( A e. RR \/ A = +oo ) )
6	5	orcanai	|- ( ( A e. ( 0 [,] +oo ) /\ -. A e. RR ) -> A = +oo )