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 ( 𝑋 ∈ ( ( 1 / 2 ) [,] 1 ) → ( ( 2 · 𝑋 ) − 1 ) ∈ ( 0 [,] 1 ) )

Proof

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