iccshftli

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

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	$⊢ (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	iccshftl	$⊢ ((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