This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iihalf1

Description: Map the first half of II into II . (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion iihalf1 ( 𝑋 ∈ ( 0 [,] ( 1 / 2 ) ) → ( 2 · 𝑋 ) ∈ ( 0 [,] 1 ) )

Proof

Step Hyp Ref Expression
1 2re ⊢ 2 ∈ ℝ
2 remulcl ⊢ ( ( 2 ∈ ℝ ∧ 𝑋 ∈ ℝ ) → ( 2 · 𝑋 ) ∈ ℝ )
3 1 2 mpan ⊢ ( 𝑋 ∈ ℝ → ( 2 · 𝑋 ) ∈ ℝ )
4 3 3ad2ant1 ⊢ ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ∧ 𝑋 ≤ ( 1 / 2 ) ) → ( 2 · 𝑋 ) ∈ ℝ )
5 0le2 ⊢ 0 ≤ 2
6 mulge0 ⊢ ( ( ( 2 ∈ ℝ ∧ 0 ≤ 2 ) ∧ ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ) → 0 ≤ ( 2 · 𝑋 ) )
7 1 5 6 mpanl12 ⊢ ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) → 0 ≤ ( 2 · 𝑋 ) )
8 7 3adant3 ⊢ ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ∧ 𝑋 ≤ ( 1 / 2 ) ) → 0 ≤ ( 2 · 𝑋 ) )
9 1re ⊢ 1 ∈ ℝ
10 2pos ⊢ 0 < 2
11 1 10 pm3.2i ⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
12 lemuldiv2 ⊢ ( ( 𝑋 ∈ ℝ ∧ 1 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 2 · 𝑋 ) ≤ 1 ↔ 𝑋 ≤ ( 1 / 2 ) ) )
13 9 11 12 mp3an23 ⊢ ( 𝑋 ∈ ℝ → ( ( 2 · 𝑋 ) ≤ 1 ↔ 𝑋 ≤ ( 1 / 2 ) ) )
14 13 biimpar ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑋 ≤ ( 1 / 2 ) ) → ( 2 · 𝑋 ) ≤ 1 )
15 14 3adant2 ⊢ ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ∧ 𝑋 ≤ ( 1 / 2 ) ) → ( 2 · 𝑋 ) ≤ 1 )
16 4 8 15 3jca ⊢ ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ∧ 𝑋 ≤ ( 1 / 2 ) ) → ( ( 2 · 𝑋 ) ∈ ℝ ∧ 0 ≤ ( 2 · 𝑋 ) ∧ ( 2 · 𝑋 ) ≤ 1 ) )
17 0re ⊢ 0 ∈ ℝ
18 halfre ⊢ ( 1 / 2 ) ∈ ℝ
19 17 18 elicc2i ⊢ ( 𝑋 ∈ ( 0 [,] ( 1 / 2 ) ) ↔ ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ∧ 𝑋 ≤ ( 1 / 2 ) ) )
20 17 9 elicc2i ⊢ ( ( 2 · 𝑋 ) ∈ ( 0 [,] 1 ) ↔ ( ( 2 · 𝑋 ) ∈ ℝ ∧ 0 ≤ ( 2 · 𝑋 ) ∧ ( 2 · 𝑋 ) ≤ 1 ) )
21 16 19 20 3imtr4i ⊢ ( 𝑋 ∈ ( 0 [,] ( 1 / 2 ) ) → ( 2 · 𝑋 ) ∈ ( 0 [,] 1 ) )