iihalf1

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

		Ref	Expression
	Assertion	iihalf1	$⊢ X \in [0, \frac{1}{2}] \to 2 X \in [0, 1]$

Step	Hyp	Ref	Expression
1		2re	$⊢ 2 \in ℝ$
2		remulcl	$⊢ (2 \in ℝ \land X \in ℝ) \to 2 X \in ℝ$
3	1 2	mpan	$⊢ X \in ℝ \to 2 X \in ℝ$
4	3	3ad2ant1	$⊢ (X \in ℝ \land 0 \leq X \land X \leq \frac{1}{2}) \to 2 X \in ℝ$
5		0le2	$⊢ 0 \leq 2$
6		mulge0	$⊢ ((2 \in ℝ \land 0 \leq 2) \land (X \in ℝ \land 0 \leq X)) \to 0 \leq 2 X$
7	1 5 6	mpanl12	$⊢ (X \in ℝ \land 0 \leq X) \to 0 \leq 2 X$
8	7	3adant3	$⊢ (X \in ℝ \land 0 \leq X \land X \leq \frac{1}{2}) \to 0 \leq 2 X$
9		1re	$⊢ 1 \in ℝ$
10		2pos	$⊢ 0 < 2$
11	1 10	pm3.2i	$⊢ (2 \in ℝ \land 0 < 2)$
12		lemuldiv2	$⊢ (X \in ℝ \land 1 \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (2 X \leq 1 \leftrightarrow X \leq \frac{1}{2})$
13	9 11 12	mp3an23	$⊢ X \in ℝ \to (2 X \leq 1 \leftrightarrow X \leq \frac{1}{2})$
14	13	biimpar	$⊢ (X \in ℝ \land X \leq \frac{1}{2}) \to 2 X \leq 1$
15	14	3adant2	$⊢ (X \in ℝ \land 0 \leq X \land X \leq \frac{1}{2}) \to 2 X \leq 1$
16	4 8 15	3jca	$⊢ (X \in ℝ \land 0 \leq X \land X \leq \frac{1}{2}) \to (2 X \in ℝ \land 0 \leq 2 X \land 2 X \leq 1)$
17		0re	$⊢ 0 \in ℝ$
18		halfre	$⊢ \frac{1}{2} \in ℝ$
19	17 18	elicc2i	$⊢ X \in [0, \frac{1}{2}] \leftrightarrow (X \in ℝ \land 0 \leq X \land X \leq \frac{1}{2})$
20	17 9	elicc2i	$⊢ 2 X \in [0, 1] \leftrightarrow (2 X \in ℝ \land 0 \leq 2 X \land 2 X \leq 1)$
21	16 19 20	3imtr4i	$⊢ X \in [0, \frac{1}{2}] \to 2 X \in [0, 1]$

Metamath Proof Explorer