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 ∈ 0 +∞

Proof

Step Hyp Ref Expression
1 0xr ⊢ 0 ∈ ℝ *
2 0le0 ⊢ 0 ≤ 0
3 elxrge0 ⊢ 0 ∈ 0 +∞ ↔ 0 ∈ ℝ * ∧ 0 ≤ 0
4 1 2 3 mpbir2an ⊢ 0 ∈ 0 +∞