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

Proof

Step Hyp Ref Expression
1 0re ⊢ 0 ∈ ℝ
2 0le0 ⊢ 0 ≤ 0
3 elrege0 ⊢ 0 ∈ 0 +∞ ↔ 0 ∈ ℝ ∧ 0 ≤ 0
4 1 2 3 mpbir2an ⊢ 0 ∈ 0 +∞