Metamath Proof Explorer

Theorem elii1

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

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

Proof

Step Hyp Ref Expression
1 0re 
 |-  0 e. RR
2 halfre 
 |-  ( 1 / 2 ) e. RR
3 1 2 elicc2i 
 |-  ( X e. ( 0 [,] ( 1 / 2 ) ) <-> ( X e. RR /\ 0 <_ X /\ X <_ ( 1 / 2 ) ) )
4 3 simp1bi 
 |-  ( X e. ( 0 [,] ( 1 / 2 ) ) -> X e. RR )
5 2 a1i 
 |-  ( X e. ( 0 [,] ( 1 / 2 ) ) -> ( 1 / 2 ) e. RR )
6 1re 
 |-  1 e. RR
7 6 a1i 
 |-  ( X e. ( 0 [,] ( 1 / 2 ) ) -> 1 e. RR )
8 3 simp3bi 
 |-  ( X e. ( 0 [,] ( 1 / 2 ) ) -> X <_ ( 1 / 2 ) )
9 halflt1 
 |-  ( 1 / 2 ) < 1
10 2 6 9 ltleii 
 |-  ( 1 / 2 ) <_ 1
11 10 a1i 
 |-  ( X e. ( 0 [,] ( 1 / 2 ) ) -> ( 1 / 2 ) <_ 1 )
12 4 5 7 8 11 letrd 
 |-  ( X e. ( 0 [,] ( 1 / 2 ) ) -> X <_ 1 )
13 12 pm4.71ri 
 |-  ( X e. ( 0 [,] ( 1 / 2 ) ) <-> ( X <_ 1 /\ X e. ( 0 [,] ( 1 / 2 ) ) ) )
14 ancom 
 |-  ( ( X <_ 1 /\ X e. ( 0 [,] ( 1 / 2 ) ) ) <-> ( X e. ( 0 [,] ( 1 / 2 ) ) /\ X <_ 1 ) )
15 an32 
 |-  ( ( ( ( X e. RR /\ 0 <_ X ) /\ X <_ ( 1 / 2 ) ) /\ X <_ 1 ) <-> ( ( ( X e. RR /\ 0 <_ X ) /\ X <_ 1 ) /\ X <_ ( 1 / 2 ) ) )
16 df-3an 
 |-  ( ( X e. RR /\ 0 <_ X /\ X <_ ( 1 / 2 ) ) <-> ( ( X e. RR /\ 0 <_ X ) /\ X <_ ( 1 / 2 ) ) )
17 3 16 bitri 
 |-  ( X e. ( 0 [,] ( 1 / 2 ) ) <-> ( ( X e. RR /\ 0 <_ X ) /\ X <_ ( 1 / 2 ) ) )
18 17 anbi1i 
 |-  ( ( X e. ( 0 [,] ( 1 / 2 ) ) /\ X <_ 1 ) <-> ( ( ( X e. RR /\ 0 <_ X ) /\ X <_ ( 1 / 2 ) ) /\ X <_ 1 ) )
19 1 6 elicc2i 
 |-  ( X e. ( 0 [,] 1 ) <-> ( X e. RR /\ 0 <_ X /\ X <_ 1 ) )
20 df-3an 
 |-  ( ( X e. RR /\ 0 <_ X /\ X <_ 1 ) <-> ( ( X e. RR /\ 0 <_ X ) /\ X <_ 1 ) )
21 19 20 bitri 
 |-  ( X e. ( 0 [,] 1 ) <-> ( ( X e. RR /\ 0 <_ X ) /\ X <_ 1 ) )
22 21 anbi1i 
 |-  ( ( X e. ( 0 [,] 1 ) /\ X <_ ( 1 / 2 ) ) <-> ( ( ( X e. RR /\ 0 <_ X ) /\ X <_ 1 ) /\ X <_ ( 1 / 2 ) ) )
23 15 18 22 3bitr4i 
 |-  ( ( X e. ( 0 [,] ( 1 / 2 ) ) /\ X <_ 1 ) <-> ( X e. ( 0 [,] 1 ) /\ X <_ ( 1 / 2 ) ) )
24 14 23 bitri 
 |-  ( ( X <_ 1 /\ X e. ( 0 [,] ( 1 / 2 ) ) ) <-> ( X e. ( 0 [,] 1 ) /\ X <_ ( 1 / 2 ) ) )
25 13 24 bitri 
 |-  ( X e. ( 0 [,] ( 1 / 2 ) ) <-> ( X e. ( 0 [,] 1 ) /\ X <_ ( 1 / 2 ) ) )