Theorem elxrge0

Description: Elementhood in the set of nonnegative extended reals. (Contributed by Mario Carneiro, 28-Jun-2014)

	Ref	Expression
Assertion	elxrge0	|- ( A e. ( 0 [,] +oo ) <-> ( A e. RR* /\ 0 <_ A ) )

Proof

Step	Hyp	Ref	Expression
1		df-3an	|- ( ( A e. RR* /\ 0 <_ A /\ A <_ +oo ) <-> ( ( A e. RR* /\ 0 <_ A ) /\ A <_ +oo ) )
2		0xr	|- 0 e. RR*
3		pnfxr	|- +oo e. RR*
4		elicc1	|- ( ( 0 e. RR* /\ +oo e. RR* ) -> ( A e. ( 0 [,] +oo ) <-> ( A e. RR* /\ 0 <_ A /\ A <_ +oo ) ) )
5	2 3 4	mp2an	|- ( A e. ( 0 [,] +oo ) <-> ( A e. RR* /\ 0 <_ A /\ A <_ +oo ) )
6		pnfge	|- ( A e. RR* -> A <_ +oo )
7	6	adantr	|- ( ( A e. RR* /\ 0 <_ A ) -> A <_ +oo )
8	7	pm4.71i	|- ( ( A e. RR* /\ 0 <_ A ) <-> ( ( A e. RR* /\ 0 <_ A ) /\ A <_ +oo ) )
9	1 5 8	3bitr4i	|- ( A e. ( 0 [,] +oo ) <-> ( A e. RR* /\ 0 <_ A ) )