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 ) )