iccdili

Description: Membership in a dilated interval. (Contributed by Jeff Madsen, 2-Sep-2009)

Step	Hyp	Ref	Expression
1		iccdili.1	$⊢ A \in ℝ$
2		iccdili.2	$⊢ B \in ℝ$
3		iccdili.3	$⊢ R \in ℝ^{+}$
4		iccdili.4	$⊢ A R = C$
5		iccdili.5	$⊢ B R = D$
6		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
7	1 2 6	mp2an	$⊢ [A, B] \subseteq ℝ$
8	7	sseli	$⊢ X \in [A, B] \to X \in ℝ$
9	4 5	iccdil	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land R \in ℝ^{+})) \to (X \in [A, B] \leftrightarrow X R \in [C, D])$
10	1 2 9	mpanl12	$⊢ (X \in ℝ \land R \in ℝ^{+}) \to (X \in [A, B] \leftrightarrow X R \in [C, D])$
11	3 10	mpan2	$⊢ X \in ℝ \to (X \in [A, B] \leftrightarrow X R \in [C, D])$
12	11	biimpd	$⊢ X \in ℝ \to (X \in [A, B] \to X R \in [C, D])$
13	8 12	mpcom	$⊢ X \in [A, B] \to X R \in [C, D]$

Metamath Proof Explorer