Metamath Proof Explorer

Theorem elxrge02

Description: Elementhood in the set of nonnegative extended reals. (Contributed by Thierry Arnoux, 18-Dec-2016)

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

Proof

Step Hyp Ref Expression
1 0xr 
 |-  0 e. RR*
2 pnfxr 
 |-  +oo e. RR*
3 0lepnf 
 |-  0 <_ +oo
4 eliccioo 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ 0 <_ +oo ) -> ( A e. ( 0 [,] +oo ) <-> ( A = 0 \/ A e. ( 0 (,) +oo ) \/ A = +oo ) ) )
5 1 2 3 4 mp3an 
 |-  ( A e. ( 0 [,] +oo ) <-> ( A = 0 \/ A e. ( 0 (,) +oo ) \/ A = +oo ) )
6 biid 
 |-  ( A = 0 <-> A = 0 )
7 ioorp 
 |-  ( 0 (,) +oo ) = RR+
8 7 eleq2i 
 |-  ( A e. ( 0 (,) +oo ) <-> A e. RR+ )
9 biid 
 |-  ( A = +oo <-> A = +oo )
10 6 8 9 3orbi123i 
 |-  ( ( A = 0 \/ A e. ( 0 (,) +oo ) \/ A = +oo ) <-> ( A = 0 \/ A e. RR+ \/ A = +oo ) )
11 5 10 bitri 
 |-  ( A e. ( 0 [,] +oo ) <-> ( A = 0 \/ A e. RR+ \/ A = +oo ) )