Description: 0 is a member of ( 0 [,) +oo ) . (Contributed by David A. Wheeler, 8-Dec-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | 0e0icopnf | ⊢ 0 ∈ ( 0 [,) +∞ ) |
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 [,) +∞ ) |