Theorem icccntri

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

	Ref	Expression
Hypotheses	icccntri.1	$$⊢A\in ℝ$$
	icccntri.2	$$⊢B\in ℝ$$
	icccntri.3	$$⊢R\in {ℝ}^{+}$$
	icccntri.4	$$⊢\frac{A}{R}=C$$
	icccntri.5	$$⊢\frac{B}{R}=D$$
Assertion	icccntri	$$⊢X\in \left[A,B\right]\to \frac{X}{R}\in \left[C,D\right]$$

Proof

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