Metamath Proof Explorer

Theorem 0e0icopnf

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

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

Proof

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