# 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}\in \left[\frac{1}{2},1\right]\to 2{X}-1\in \left[0,1\right]$

### Proof

Step Hyp Ref Expression
1 2re ${⊢}2\in ℝ$
2 remulcl ${⊢}\left(2\in ℝ\wedge {X}\in ℝ\right)\to 2{X}\in ℝ$
3 1 2 mpan ${⊢}{X}\in ℝ\to 2{X}\in ℝ$
4 1re ${⊢}1\in ℝ$
5 resubcl ${⊢}\left(2{X}\in ℝ\wedge 1\in ℝ\right)\to 2{X}-1\in ℝ$
6 3 4 5 sylancl ${⊢}{X}\in ℝ\to 2{X}-1\in ℝ$
7 6 3ad2ant1 ${⊢}\left({X}\in ℝ\wedge \frac{1}{2}\le {X}\wedge {X}\le 1\right)\to 2{X}-1\in ℝ$
8 subge0 ${⊢}\left(2{X}\in ℝ\wedge 1\in ℝ\right)\to \left(0\le 2{X}-1↔1\le 2{X}\right)$
9 3 4 8 sylancl ${⊢}{X}\in ℝ\to \left(0\le 2{X}-1↔1\le 2{X}\right)$
10 2pos ${⊢}0<2$
11 1 10 pm3.2i ${⊢}\left(2\in ℝ\wedge 0<2\right)$
12 ledivmul ${⊢}\left(1\in ℝ\wedge {X}\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left(\frac{1}{2}\le {X}↔1\le 2{X}\right)$
13 4 11 12 mp3an13 ${⊢}{X}\in ℝ\to \left(\frac{1}{2}\le {X}↔1\le 2{X}\right)$
14 9 13 bitr4d ${⊢}{X}\in ℝ\to \left(0\le 2{X}-1↔\frac{1}{2}\le {X}\right)$
15 14 biimpar ${⊢}\left({X}\in ℝ\wedge \frac{1}{2}\le {X}\right)\to 0\le 2{X}-1$
16 15 3adant3 ${⊢}\left({X}\in ℝ\wedge \frac{1}{2}\le {X}\wedge {X}\le 1\right)\to 0\le 2{X}-1$
17 ax-1cn ${⊢}1\in ℂ$
18 17 2timesi ${⊢}2\cdot 1=1+1$
19 18 a1i ${⊢}{X}\in ℝ\to 2\cdot 1=1+1$
20 19 breq2d ${⊢}{X}\in ℝ\to \left(2{X}\le 2\cdot 1↔2{X}\le 1+1\right)$
21 lemul2 ${⊢}\left({X}\in ℝ\wedge 1\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left({X}\le 1↔2{X}\le 2\cdot 1\right)$
22 4 11 21 mp3an23 ${⊢}{X}\in ℝ\to \left({X}\le 1↔2{X}\le 2\cdot 1\right)$
23 lesubadd ${⊢}\left(2{X}\in ℝ\wedge 1\in ℝ\wedge 1\in ℝ\right)\to \left(2{X}-1\le 1↔2{X}\le 1+1\right)$
24 4 4 23 mp3an23 ${⊢}2{X}\in ℝ\to \left(2{X}-1\le 1↔2{X}\le 1+1\right)$
25 3 24 syl ${⊢}{X}\in ℝ\to \left(2{X}-1\le 1↔2{X}\le 1+1\right)$
26 20 22 25 3bitr4d ${⊢}{X}\in ℝ\to \left({X}\le 1↔2{X}-1\le 1\right)$
27 26 biimpa ${⊢}\left({X}\in ℝ\wedge {X}\le 1\right)\to 2{X}-1\le 1$
28 27 3adant2 ${⊢}\left({X}\in ℝ\wedge \frac{1}{2}\le {X}\wedge {X}\le 1\right)\to 2{X}-1\le 1$
29 7 16 28 3jca ${⊢}\left({X}\in ℝ\wedge \frac{1}{2}\le {X}\wedge {X}\le 1\right)\to \left(2{X}-1\in ℝ\wedge 0\le 2{X}-1\wedge 2{X}-1\le 1\right)$
30 halfre ${⊢}\frac{1}{2}\in ℝ$
31 30 4 elicc2i ${⊢}{X}\in \left[\frac{1}{2},1\right]↔\left({X}\in ℝ\wedge \frac{1}{2}\le {X}\wedge {X}\le 1\right)$
32 elicc01 ${⊢}2{X}-1\in \left[0,1\right]↔\left(2{X}-1\in ℝ\wedge 0\le 2{X}-1\wedge 2{X}-1\le 1\right)$
33 29 31 32 3imtr4i ${⊢}{X}\in \left[\frac{1}{2},1\right]\to 2{X}-1\in \left[0,1\right]$