Metamath Proof Explorer

Theorem elii2

Description: Divide the unit interval into two pieces. (Contributed by Mario Carneiro, 7-Jun-2014)

Ref Expression
Assertion elii2 
|- ( ( X e. ( 0 [,] 1 ) /\ -. X <_ ( 1 / 2 ) ) -> X e. ( ( 1 / 2 ) [,] 1 ) )

Proof

Step Hyp Ref Expression
1 elicc01 
 |-  ( X e. ( 0 [,] 1 ) <-> ( X e. RR /\ 0 <_ X /\ X <_ 1 ) )
2 1 simp1bi 
 |-  ( X e. ( 0 [,] 1 ) -> X e. RR )
3 2 adantr 
 |-  ( ( X e. ( 0 [,] 1 ) /\ -. X <_ ( 1 / 2 ) ) -> X e. RR )
4 halfre 
 |-  ( 1 / 2 ) e. RR
5 letric 
 |-  ( ( X e. RR /\ ( 1 / 2 ) e. RR ) -> ( X <_ ( 1 / 2 ) \/ ( 1 / 2 ) <_ X ) )
6 2 4 5 sylancl 
 |-  ( X e. ( 0 [,] 1 ) -> ( X <_ ( 1 / 2 ) \/ ( 1 / 2 ) <_ X ) )
7 6 orcanai 
 |-  ( ( X e. ( 0 [,] 1 ) /\ -. X <_ ( 1 / 2 ) ) -> ( 1 / 2 ) <_ X )
8 1 simp3bi 
 |-  ( X e. ( 0 [,] 1 ) -> X <_ 1 )
9 8 adantr 
 |-  ( ( X e. ( 0 [,] 1 ) /\ -. X <_ ( 1 / 2 ) ) -> X <_ 1 )
10 1re 
 |-  1 e. RR
11 4 10 elicc2i 
 |-  ( X e. ( ( 1 / 2 ) [,] 1 ) <-> ( X e. RR /\ ( 1 / 2 ) <_ X /\ X <_ 1 ) )
12 3 7 9 11 syl3anbrc 
 |-  ( ( X e. ( 0 [,] 1 ) /\ -. X <_ ( 1 / 2 ) ) -> X e. ( ( 1 / 2 ) [,] 1 ) )