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 00+∞

Proof

Step Hyp Ref Expression
1 0xr 0*
2 0le0 00
3 elxrge0 00+∞0*00
4 1 2 3 mpbir2an 00+∞