Theorem 0elunit

Description: Zero is an element of the closed unit interval. (Contributed by Scott Fenton, 11-Jun-2013)

	Ref	Expression
Assertion	0elunit	⊢ 0 ∈ ( 0 [,] 1 )

Proof

Step	Hyp	Ref	Expression
1		0re	⊢ 0 ∈ ℝ
2		0le0	⊢ 0 ≤ 0
3		0le1	⊢ 0 ≤ 1
4		elicc01	⊢ ( 0 ∈ ( 0 [,] 1 ) ↔ ( 0 ∈ ℝ ∧ 0 ≤ 0 ∧ 0 ≤ 1 ) )
5	1 2 3 4	mpbir3an	⊢ 0 ∈ ( 0 [,] 1 )