Metamath Proof Explorer

Theorem 1elunit

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

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

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