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 e. ( 0 [,] 1 )

Proof

Step Hyp Ref Expression
1 0re 
 |-  0 e. RR
2 0le0 
 |-  0 <_ 0
3 0le1 
 |-  0 <_ 1
4 elicc01 
 |-  ( 0 e. ( 0 [,] 1 ) <-> ( 0 e. RR /\ 0 <_ 0 /\ 0 <_ 1 ) )
5 1 2 3 4 mpbir3an 
 |-  0 e. ( 0 [,] 1 )