iccshftri

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

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	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
7	1 2 6	mp2an	$⊢ [A, B] \subseteq ℝ$
8	7	sseli	$⊢ X \in [A, B] \to X \in ℝ$
9	4 5	iccshftr	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land R \in ℝ)) \to (X \in [A, B] \leftrightarrow X + R \in [C, D])$
10	1 2 9	mpanl12	$⊢ (X \in ℝ \land R \in ℝ) \to (X \in [A, B] \leftrightarrow X + R \in [C, D])$
11	3 10	mpan2	$⊢ X \in ℝ \to (X \in [A, B] \leftrightarrow X + R \in [C, D])$
12	11	biimpd	$⊢ X \in ℝ \to (X \in [A, B] \to X + R \in [C, D])$
13	8 12	mpcom	$⊢ X \in [A, B] \to X + R \in [C, D]$

Metamath Proof Explorer