Theorem iccshftri

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

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

Proof

Step	Hyp	Ref	Expression
1		iccshftri.1	$$⊢A\in ℝ$$
2		iccshftri.2	$$⊢B\in ℝ$$
3		iccshftri.3	$$⊢R\in ℝ$$
4		iccshftri.4	$$⊢A+R=C$$
5		iccshftri.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	iccshftr	$$⊢\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]$$