iccdil

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

	Ref	Expression
Hypotheses	iccdil.1	$⊢ A R = C$
	iccdil.2	$⊢ B R = D$
Assertion	iccdil	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land R \in ℝ^{+})) \to (X \in [A, B] \leftrightarrow X R \in [C, D])$

Proof

Step	Hyp	Ref	Expression
1		iccdil.1	$⊢ A R = C$
2		iccdil.2	$⊢ B R = D$
3		simpl	$⊢ (X \in ℝ \land R \in ℝ^{+}) \to X \in ℝ$
4		rpre	$⊢ R \in ℝ^{+} \to R \in ℝ$
5		remulcl	$⊢ (X \in ℝ \land R \in ℝ) \to X R \in ℝ$
6	4 5	sylan2	$⊢ (X \in ℝ \land R \in ℝ^{+}) \to X R \in ℝ$
7	3 6	2thd	$⊢ (X \in ℝ \land R \in ℝ^{+}) \to (X \in ℝ \leftrightarrow X R \in ℝ)$
8	7	adantl	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land R \in ℝ^{+})) \to (X \in ℝ \leftrightarrow X R \in ℝ)$
9		elrp	$⊢ R \in ℝ^{+} \leftrightarrow (R \in ℝ \land 0 < R)$
10		lemul1	$⊢ (A \in ℝ \land X \in ℝ \land (R \in ℝ \land 0 < R)) \to (A \leq X \leftrightarrow A R \leq X R)$
11	9 10	syl3an3b	$⊢ (A \in ℝ \land X \in ℝ \land R \in ℝ^{+}) \to (A \leq X \leftrightarrow A R \leq X R)$
12	11	3expb	$⊢ (A \in ℝ \land (X \in ℝ \land R \in ℝ^{+})) \to (A \leq X \leftrightarrow A R \leq X R)$
13	12	adantlr	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land R \in ℝ^{+})) \to (A \leq X \leftrightarrow A R \leq X R)$
14	1	breq1i	$⊢ A R \leq X R \leftrightarrow C \leq X R$
15	13 14	bitrdi	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land R \in ℝ^{+})) \to (A \leq X \leftrightarrow C \leq X R)$
16		lemul1	$⊢ (X \in ℝ \land B \in ℝ \land (R \in ℝ \land 0 < R)) \to (X \leq B \leftrightarrow X R \leq B R)$
17	9 16	syl3an3b	$⊢ (X \in ℝ \land B \in ℝ \land R \in ℝ^{+}) \to (X \leq B \leftrightarrow X R \leq B R)$
18	17	3expb	$⊢ (X \in ℝ \land (B \in ℝ \land R \in ℝ^{+})) \to (X \leq B \leftrightarrow X R \leq B R)$
19	18	an12s	$⊢ (B \in ℝ \land (X \in ℝ \land R \in ℝ^{+})) \to (X \leq B \leftrightarrow X R \leq B R)$
20	19	adantll	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land R \in ℝ^{+})) \to (X \leq B \leftrightarrow X R \leq B R)$
21	2	breq2i	$⊢ X R \leq B R \leftrightarrow X R \leq D$
22	20 21	bitrdi	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land R \in ℝ^{+})) \to (X \leq B \leftrightarrow X R \leq D)$
23	8 15 22	3anbi123d	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land R \in ℝ^{+})) \to ((X \in ℝ \land A \leq X \land X \leq B) \leftrightarrow (X R \in ℝ \land C \leq X R \land X R \leq D))$
24		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (X \in [A, B] \leftrightarrow (X \in ℝ \land A \leq X \land X \leq B))$
25	24	adantr	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land R \in ℝ^{+})) \to (X \in [A, B] \leftrightarrow (X \in ℝ \land A \leq X \land X \leq B))$
26		remulcl	$⊢ (A \in ℝ \land R \in ℝ) \to A R \in ℝ$
27	1 26	eqeltrrid	$⊢ (A \in ℝ \land R \in ℝ) \to C \in ℝ$
28		remulcl	$⊢ (B \in ℝ \land R \in ℝ) \to B R \in ℝ$
29	2 28	eqeltrrid	$⊢ (B \in ℝ \land R \in ℝ) \to D \in ℝ$
30		elicc2	$⊢ (C \in ℝ \land D \in ℝ) \to (X R \in [C, D] \leftrightarrow (X R \in ℝ \land C \leq X R \land X R \leq D))$
31	27 29 30	syl2an	$⊢ ((A \in ℝ \land R \in ℝ) \land (B \in ℝ \land R \in ℝ)) \to (X R \in [C, D] \leftrightarrow (X R \in ℝ \land C \leq X R \land X R \leq D))$
32	31	anandirs	$⊢ ((A \in ℝ \land B \in ℝ) \land R \in ℝ) \to (X R \in [C, D] \leftrightarrow (X R \in ℝ \land C \leq X R \land X R \leq D))$
33	4 32	sylan2	$⊢ ((A \in ℝ \land B \in ℝ) \land R \in ℝ^{+}) \to (X R \in [C, D] \leftrightarrow (X R \in ℝ \land C \leq X R \land X R \leq D))$
34	33	adantrl	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land R \in ℝ^{+})) \to (X R \in [C, D] \leftrightarrow (X R \in ℝ \land C \leq X R \land X R \leq D))$
35	23 25 34	3bitr4d	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land R \in ℝ^{+})) \to (X \in [A, B] \leftrightarrow X R \in [C, D])$

Metamath Proof Explorer

Theorem iccdil

Proof