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

Metamath Proof Explorer

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