Theorem 1elunit

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

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

Proof

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