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∈121→2⁢X−1∈01

Proof

Step Hyp Ref Expression
1 2re ⊢2∈ℝ
2 remulcl ⊢2∈ℝ∧X∈ℝ→2⁢X∈ℝ
3 1 2 mpan ⊢X∈ℝ→2⁢X∈ℝ
4 1re ⊢1∈ℝ
5 resubcl ⊢2⁢X∈ℝ∧1∈ℝ→2⁢X−1∈ℝ
6 3 4 5 sylancl ⊢X∈ℝ→2⁢X−1∈ℝ
7 6 3ad2ant1 ⊢X∈ℝ∧12≤X∧X≤1→2⁢X−1∈ℝ
8 subge0 ⊢2⁢X∈ℝ∧1∈ℝ→0≤2⁢X−1↔1≤2⁢X
9 3 4 8 sylancl ⊢X∈ℝ→0≤2⁢X−1↔1≤2⁢X
10 2pos ⊢0<2
11 1 10 pm3.2i ⊢2∈ℝ∧0<2
12 ledivmul ⊢1∈ℝ∧X∈ℝ∧2∈ℝ∧0<2→12≤X↔1≤2⁢X
13 4 11 12 mp3an13 ⊢X∈ℝ→12≤X↔1≤2⁢X
14 9 13 bitr4d ⊢X∈ℝ→0≤2⁢X−1↔12≤X
15 14 biimpar ⊢X∈ℝ∧12≤X→0≤2⁢X−1
16 15 3adant3 ⊢X∈ℝ∧12≤X∧X≤1→0≤2⁢X−1
17 ax-1cn ⊢1∈ℂ
18 17 2timesi ⊢2⋅1=1+1
19 18 a1i ⊢X∈ℝ→2⋅1=1+1
20 19 breq2d ⊢X∈ℝ→2⁢X≤2⋅1↔2⁢X≤1+1
21 lemul2 ⊢X∈ℝ∧1∈ℝ∧2∈ℝ∧0<2→X≤1↔2⁢X≤2⋅1
22 4 11 21 mp3an23 ⊢X∈ℝ→X≤1↔2⁢X≤2⋅1
23 lesubadd ⊢2⁢X∈ℝ∧1∈ℝ∧1∈ℝ→2⁢X−1≤1↔2⁢X≤1+1
24 4 4 23 mp3an23 ⊢2⁢X∈ℝ→2⁢X−1≤1↔2⁢X≤1+1
25 3 24 syl ⊢X∈ℝ→2⁢X−1≤1↔2⁢X≤1+1
26 20 22 25 3bitr4d ⊢X∈ℝ→X≤1↔2⁢X−1≤1
27 26 biimpa ⊢X∈ℝ∧X≤1→2⁢X−1≤1
28 27 3adant2 ⊢X∈ℝ∧12≤X∧X≤1→2⁢X−1≤1
29 7 16 28 3jca ⊢X∈ℝ∧12≤X∧X≤1→2⁢X−1∈ℝ∧0≤2⁢X−1∧2⁢X−1≤1
30 halfre ⊢12∈ℝ
31 30 4 elicc2i ⊢X∈121↔X∈ℝ∧12≤X∧X≤1
32 elicc01 ⊢2⁢X−1∈01↔2⁢X−1∈ℝ∧0≤2⁢X−1∧2⁢X−1≤1
33 29 31 32 3imtr4i ⊢X∈121→2⁢X−1∈01