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 [,] +∞ )