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

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 ∈ ℝ ∧ 1 2 ≤ 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 → 1 2 ≤ X ↔ 1 ≤ 2 ⁢ X
13 4 11 12 mp3an13 ⊢ X ∈ ℝ → 1 2 ≤ X ↔ 1 ≤ 2 ⁢ X
14 9 13 bitr4d ⊢ X ∈ ℝ → 0 ≤ 2 ⁢ X − 1 ↔ 1 2 ≤ X
15 14 biimpar ⊢ X ∈ ℝ ∧ 1 2 ≤ X → 0 ≤ 2 ⁢ X − 1
16 15 3adant3 ⊢ X ∈ ℝ ∧ 1 2 ≤ 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 ∈ ℝ ∧ 1 2 ≤ X ∧ X ≤ 1 → 2 ⁢ X − 1 ≤ 1
29 7 16 28 3jca ⊢ X ∈ ℝ ∧ 1 2 ≤ X ∧ X ≤ 1 → 2 ⁢ X − 1 ∈ ℝ ∧ 0 ≤ 2 ⁢ X − 1 ∧ 2 ⁢ X − 1 ≤ 1
30 halfre ⊢ 1 2 ∈ ℝ
31 30 4 elicc2i ⊢ X ∈ 1 2 1 ↔ X ∈ ℝ ∧ 1 2 ≤ X ∧ X ≤ 1
32 elicc01 ⊢ 2 ⁢ X − 1 ∈ 0 1 ↔ 2 ⁢ X − 1 ∈ ℝ ∧ 0 ≤ 2 ⁢ X − 1 ∧ 2 ⁢ X − 1 ≤ 1
33 29 31 32 3imtr4i ⊢ X ∈ 1 2 1 → 2 ⁢ X − 1 ∈ 0 1