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 ) )