Theorem iccshftli

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

	Ref	Expression
Hypotheses	iccshftli.1	$$⊢A\in ℝ$$
	iccshftli.2	$$⊢B\in ℝ$$
	iccshftli.3	$$⊢R\in ℝ$$
	iccshftli.4	$$⊢A-R=C$$
	iccshftli.5	$$⊢B-R=D$$
Assertion	iccshftli	$$⊢X\in \left[A,B\right]\to X-R\in \left[C,D\right]$$

Proof

Step	Hyp	Ref	Expression
1		iccshftli.1	$$⊢A\in ℝ$$
2		iccshftli.2	$$⊢B\in ℝ$$
3		iccshftli.3	$$⊢R\in ℝ$$
4		iccshftli.4	$$⊢A-R=C$$
5		iccshftli.5	$$⊢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	iccshftl	$$⊢\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 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 X-R\in \left[C,D\right]\right)$$
11	3 10	mpan2	$$⊢X\in ℝ\to \left(X\in \left[A,B\right]\leftrightarrow X-R\in \left[C,D\right]\right)$$
12	11	biimpd	$$⊢X\in ℝ\to \left(X\in \left[A,B\right]\to X-R\in \left[C,D\right]\right)$$
13	8 12	mpcom	$$⊢X\in \left[A,B\right]\to X-R\in \left[C,D\right]$$