Metamath Proof Explorer

Theorem iihalf1

Description: Map the first half of II into II . (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion iihalf1 
|- ( X e. ( 0 [,] ( 1 / 2 ) ) -> ( 2 x. X ) e. ( 0 [,] 1 ) )

Proof

Step Hyp Ref Expression
1 2re 
 |-  2 e. RR
2 remulcl 
 |-  ( ( 2 e. RR /\ X e. RR ) -> ( 2 x. X ) e. RR )
3 1 2 mpan 
 |-  ( X e. RR -> ( 2 x. X ) e. RR )
4 3 3ad2ant1 
 |-  ( ( X e. RR /\ 0 <_ X /\ X <_ ( 1 / 2 ) ) -> ( 2 x. X ) e. RR )
5 0le2 
 |-  0 <_ 2
6 mulge0 
 |-  ( ( ( 2 e. RR /\ 0 <_ 2 ) /\ ( X e. RR /\ 0 <_ X ) ) -> 0 <_ ( 2 x. X ) )
7 1 5 6 mpanl12 
 |-  ( ( X e. RR /\ 0 <_ X ) -> 0 <_ ( 2 x. X ) )
8 7 3adant3 
 |-  ( ( X e. RR /\ 0 <_ X /\ X <_ ( 1 / 2 ) ) -> 0 <_ ( 2 x. X ) )
9 1re 
 |-  1 e. RR
10 2pos 
 |-  0 < 2
11 1 10 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
12 lemuldiv2 
 |-  ( ( X e. RR /\ 1 e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 2 x. X ) <_ 1 <-> X <_ ( 1 / 2 ) ) )
13 9 11 12 mp3an23 
 |-  ( X e. RR -> ( ( 2 x. X ) <_ 1 <-> X <_ ( 1 / 2 ) ) )
14 13 biimpar 
 |-  ( ( X e. RR /\ X <_ ( 1 / 2 ) ) -> ( 2 x. X ) <_ 1 )
15 14 3adant2 
 |-  ( ( X e. RR /\ 0 <_ X /\ X <_ ( 1 / 2 ) ) -> ( 2 x. X ) <_ 1 )
16 4 8 15 3jca 
 |-  ( ( X e. RR /\ 0 <_ X /\ X <_ ( 1 / 2 ) ) -> ( ( 2 x. X ) e. RR /\ 0 <_ ( 2 x. X ) /\ ( 2 x. X ) <_ 1 ) )
17 0re 
 |-  0 e. RR
18 halfre 
 |-  ( 1 / 2 ) e. RR
19 17 18 elicc2i 
 |-  ( X e. ( 0 [,] ( 1 / 2 ) ) <-> ( X e. RR /\ 0 <_ X /\ X <_ ( 1 / 2 ) ) )
20 17 9 elicc2i 
 |-  ( ( 2 x. X ) e. ( 0 [,] 1 ) <-> ( ( 2 x. X ) e. RR /\ 0 <_ ( 2 x. X ) /\ ( 2 x. X ) <_ 1 ) )
21 16 19 20 3imtr4i 
 |-  ( X e. ( 0 [,] ( 1 / 2 ) ) -> ( 2 x. X ) e. ( 0 [,] 1 ) )