This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iihalf2

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

Ref Expression
Assertion iihalf2 
|- ( X e. ( ( 1 / 2 ) [,] 1 ) -> ( ( 2 x. X ) - 1 ) 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 1re 
 |-  1 e. RR
5 resubcl 
 |-  ( ( ( 2 x. X ) e. RR /\ 1 e. RR ) -> ( ( 2 x. X ) - 1 ) e. RR )
6 3 4 5 sylancl 
 |-  ( X e. RR -> ( ( 2 x. X ) - 1 ) e. RR )
7 6 3ad2ant1 
 |-  ( ( X e. RR /\ ( 1 / 2 ) <_ X /\ X <_ 1 ) -> ( ( 2 x. X ) - 1 ) e. RR )
8 subge0 
 |-  ( ( ( 2 x. X ) e. RR /\ 1 e. RR ) -> ( 0 <_ ( ( 2 x. X ) - 1 ) <-> 1 <_ ( 2 x. X ) ) )
9 3 4 8 sylancl 
 |-  ( X e. RR -> ( 0 <_ ( ( 2 x. X ) - 1 ) <-> 1 <_ ( 2 x. X ) ) )
10 2pos 
 |-  0 < 2
11 1 10 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
12 ledivmul 
 |-  ( ( 1 e. RR /\ X e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 1 / 2 ) <_ X <-> 1 <_ ( 2 x. X ) ) )
13 4 11 12 mp3an13 
 |-  ( X e. RR -> ( ( 1 / 2 ) <_ X <-> 1 <_ ( 2 x. X ) ) )
14 9 13 bitr4d 
 |-  ( X e. RR -> ( 0 <_ ( ( 2 x. X ) - 1 ) <-> ( 1 / 2 ) <_ X ) )
15 14 biimpar 
 |-  ( ( X e. RR /\ ( 1 / 2 ) <_ X ) -> 0 <_ ( ( 2 x. X ) - 1 ) )
16 15 3adant3 
 |-  ( ( X e. RR /\ ( 1 / 2 ) <_ X /\ X <_ 1 ) -> 0 <_ ( ( 2 x. X ) - 1 ) )
17 ax-1cn 
 |-  1 e. CC
18 17 2timesi 
 |-  ( 2 x. 1 ) = ( 1 + 1 )
19 18 a1i 
 |-  ( X e. RR -> ( 2 x. 1 ) = ( 1 + 1 ) )
20 19 breq2d 
 |-  ( X e. RR -> ( ( 2 x. X ) <_ ( 2 x. 1 ) <-> ( 2 x. X ) <_ ( 1 + 1 ) ) )
21 lemul2 
 |-  ( ( X e. RR /\ 1 e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( X <_ 1 <-> ( 2 x. X ) <_ ( 2 x. 1 ) ) )
22 4 11 21 mp3an23 
 |-  ( X e. RR -> ( X <_ 1 <-> ( 2 x. X ) <_ ( 2 x. 1 ) ) )
23 lesubadd 
 |-  ( ( ( 2 x. X ) e. RR /\ 1 e. RR /\ 1 e. RR ) -> ( ( ( 2 x. X ) - 1 ) <_ 1 <-> ( 2 x. X ) <_ ( 1 + 1 ) ) )
24 4 4 23 mp3an23 
 |-  ( ( 2 x. X ) e. RR -> ( ( ( 2 x. X ) - 1 ) <_ 1 <-> ( 2 x. X ) <_ ( 1 + 1 ) ) )
25 3 24 syl 
 |-  ( X e. RR -> ( ( ( 2 x. X ) - 1 ) <_ 1 <-> ( 2 x. X ) <_ ( 1 + 1 ) ) )
26 20 22 25 3bitr4d 
 |-  ( X e. RR -> ( X <_ 1 <-> ( ( 2 x. X ) - 1 ) <_ 1 ) )
27 26 biimpa 
 |-  ( ( X e. RR /\ X <_ 1 ) -> ( ( 2 x. X ) - 1 ) <_ 1 )
28 27 3adant2 
 |-  ( ( X e. RR /\ ( 1 / 2 ) <_ X /\ X <_ 1 ) -> ( ( 2 x. X ) - 1 ) <_ 1 )
29 7 16 28 3jca 
 |-  ( ( X e. RR /\ ( 1 / 2 ) <_ X /\ X <_ 1 ) -> ( ( ( 2 x. X ) - 1 ) e. RR /\ 0 <_ ( ( 2 x. X ) - 1 ) /\ ( ( 2 x. X ) - 1 ) <_ 1 ) )
30 halfre 
 |-  ( 1 / 2 ) e. RR
31 30 4 elicc2i 
 |-  ( X e. ( ( 1 / 2 ) [,] 1 ) <-> ( X e. RR /\ ( 1 / 2 ) <_ X /\ X <_ 1 ) )
32 elicc01 
 |-  ( ( ( 2 x. X ) - 1 ) e. ( 0 [,] 1 ) <-> ( ( ( 2 x. X ) - 1 ) e. RR /\ 0 <_ ( ( 2 x. X ) - 1 ) /\ ( ( 2 x. X ) - 1 ) <_ 1 ) )
33 29 31 32 3imtr4i 
 |-  ( X e. ( ( 1 / 2 ) [,] 1 ) -> ( ( 2 x. X ) - 1 ) e. ( 0 [,] 1 ) )