icccntr

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

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

Proof

Step	Hyp	Ref	Expression
1		icccntr.1	$⊢ \frac{A}{R} = C$
2		icccntr.2	$⊢ \frac{B}{R} = D$
3		simpl	$⊢ (X \in ℝ \land R \in ℝ^{+}) \to X \in ℝ$
4		rerpdivcl	$⊢ (X \in ℝ \land R \in ℝ^{+}) \to \frac{X}{R} \in ℝ$
5	3 4	2thd	$⊢ (X \in ℝ \land R \in ℝ^{+}) \to (X \in ℝ \leftrightarrow \frac{X}{R} \in ℝ)$
6	5	adantl	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land R \in ℝ^{+})) \to (X \in ℝ \leftrightarrow \frac{X}{R} \in ℝ)$
7		elrp	$⊢ R \in ℝ^{+} \leftrightarrow (R \in ℝ \land 0 < R)$
8		lediv1	$⊢ (A \in ℝ \land X \in ℝ \land (R \in ℝ \land 0 < R)) \to (A \leq X \leftrightarrow \frac{A}{R} \leq \frac{X}{R})$
9	7 8	syl3an3b	$⊢ (A \in ℝ \land X \in ℝ \land R \in ℝ^{+}) \to (A \leq X \leftrightarrow \frac{A}{R} \leq \frac{X}{R})$
10	9	3expb	$⊢ (A \in ℝ \land (X \in ℝ \land R \in ℝ^{+})) \to (A \leq X \leftrightarrow \frac{A}{R} \leq \frac{X}{R})$
11	10	adantlr	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land R \in ℝ^{+})) \to (A \leq X \leftrightarrow \frac{A}{R} \leq \frac{X}{R})$
12	1	breq1i	$⊢ \frac{A}{R} \leq \frac{X}{R} \leftrightarrow C \leq \frac{X}{R}$
13	11 12	syl6bb	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land R \in ℝ^{+})) \to (A \leq X \leftrightarrow C \leq \frac{X}{R})$
14		lediv1	$⊢ (X \in ℝ \land B \in ℝ \land (R \in ℝ \land 0 < R)) \to (X \leq B \leftrightarrow \frac{X}{R} \leq \frac{B}{R})$
15	7 14	syl3an3b	$⊢ (X \in ℝ \land B \in ℝ \land R \in ℝ^{+}) \to (X \leq B \leftrightarrow \frac{X}{R} \leq \frac{B}{R})$
16	15	3expb	$⊢ (X \in ℝ \land (B \in ℝ \land R \in ℝ^{+})) \to (X \leq B \leftrightarrow \frac{X}{R} \leq \frac{B}{R})$
17	16	an12s	$⊢ (B \in ℝ \land (X \in ℝ \land R \in ℝ^{+})) \to (X \leq B \leftrightarrow \frac{X}{R} \leq \frac{B}{R})$
18	17	adantll	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land R \in ℝ^{+})) \to (X \leq B \leftrightarrow \frac{X}{R} \leq \frac{B}{R})$
19	2	breq2i	$⊢ \frac{X}{R} \leq \frac{B}{R} \leftrightarrow \frac{X}{R} \leq D$
20	18 19	syl6bb	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land R \in ℝ^{+})) \to (X \leq B \leftrightarrow \frac{X}{R} \leq D)$
21	6 13 20	3anbi123d	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land R \in ℝ^{+})) \to ((X \in ℝ \land A \leq X \land X \leq B) \leftrightarrow (\frac{X}{R} \in ℝ \land C \leq \frac{X}{R} \land \frac{X}{R} \leq D))$
22		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (X \in [A, B] \leftrightarrow (X \in ℝ \land A \leq X \land X \leq B))$
23	22	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))$
24		rerpdivcl	$⊢ (A \in ℝ \land R \in ℝ^{+}) \to \frac{A}{R} \in ℝ$
25	1 24	eqeltrrid	$⊢ (A \in ℝ \land R \in ℝ^{+}) \to C \in ℝ$
26		rerpdivcl	$⊢ (B \in ℝ \land R \in ℝ^{+}) \to \frac{B}{R} \in ℝ$
27	2 26	eqeltrrid	$⊢ (B \in ℝ \land R \in ℝ^{+}) \to D \in ℝ$
28		elicc2	$⊢ (C \in ℝ \land D \in ℝ) \to (\frac{X}{R} \in [C, D] \leftrightarrow (\frac{X}{R} \in ℝ \land C \leq \frac{X}{R} \land \frac{X}{R} \leq D))$
29	25 27 28	syl2an	$⊢ ((A \in ℝ \land R \in ℝ^{+}) \land (B \in ℝ \land R \in ℝ^{+})) \to (\frac{X}{R} \in [C, D] \leftrightarrow (\frac{X}{R} \in ℝ \land C \leq \frac{X}{R} \land \frac{X}{R} \leq D))$
30	29	anandirs	$⊢ ((A \in ℝ \land B \in ℝ) \land R \in ℝ^{+}) \to (\frac{X}{R} \in [C, D] \leftrightarrow (\frac{X}{R} \in ℝ \land C \leq \frac{X}{R} \land \frac{X}{R} \leq D))$
31	30	adantrl	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land R \in ℝ^{+})) \to (\frac{X}{R} \in [C, D] \leftrightarrow (\frac{X}{R} \in ℝ \land C \leq \frac{X}{R} \land \frac{X}{R} \leq D))$
32	21 23 31	3bitr4d	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land R \in ℝ^{+})) \to (X \in [A, B] \leftrightarrow \frac{X}{R} \in [C, D])$

Metamath Proof Explorer

Theorem icccntr

Proof