Metamath Proof Explorer

Theorem 0e0iccpnf

Description: 0 is a member of ( 0 , +oo ) . (Contributed by David A. Wheeler, 8-Dec-2018)

Ref Expression
Assertion 0e0iccpnf 
|- 0 e. ( 0 [,] +oo )

Proof

Step Hyp Ref Expression
1 0xr 
 |-  0 e. RR*
2 0le0 
 |-  0 <_ 0
3 elxrge0 
 |-  ( 0 e. ( 0 [,] +oo ) <-> ( 0 e. RR* /\ 0 <_ 0 ) )
4 1 2 3 mpbir2an 
 |-  0 e. ( 0 [,] +oo )