Metamath Proof Explorer

Theorem 0elunit

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

		Ref	Expression
	Assertion	0elunit	$⊢ 0 \in [0, 1]$

Step	Hyp	Ref	Expression
1		0re	$⊢ 0 \in ℝ$
2		0le0	$⊢ 0 \leq 0$
3		0le1	$⊢ 0 \leq 1$
4		elicc01	$⊢ 0 \in [0, 1] \leftrightarrow (0 \in ℝ \land 0 \leq 0 \land 0 \leq 1)$
5	1 2 3 4	mpbir3an	$⊢ 0 \in [0, 1]$