eliooshift

Description: Element of an open interval shifted by a displacement. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	eliooshift.a	$⊢ φ \to A \in ℝ$
	eliooshift.b	$⊢ φ \to B \in ℝ$
	eliooshift.c	$⊢ φ \to C \in ℝ$
	eliooshift.d	$⊢ φ \to D \in ℝ$
Assertion	eliooshift	$⊢ φ \to (A \in (B, C) \leftrightarrow A + D \in (B + D, C + D))$

Step	Hyp	Ref	Expression
1		eliooshift.a	$⊢ φ \to A \in ℝ$
2		eliooshift.b	$⊢ φ \to B \in ℝ$
3		eliooshift.c	$⊢ φ \to C \in ℝ$
4		eliooshift.d	$⊢ φ \to D \in ℝ$
5	1 4	readdcld	$⊢ φ \to A + D \in ℝ$
6	5 1	2thd	$⊢ φ \to (A + D \in ℝ \leftrightarrow A \in ℝ)$
7	2 1 4	ltadd1d	$⊢ φ \to (B < A \leftrightarrow B + D < A + D)$
8	7	bicomd	$⊢ φ \to (B + D < A + D \leftrightarrow B < A)$
9	1 3 4	ltadd1d	$⊢ φ \to (A < C \leftrightarrow A + D < C + D)$
10	9	bicomd	$⊢ φ \to (A + D < C + D \leftrightarrow A < C)$
11	6 8 10	3anbi123d	$⊢ φ \to ((A + D \in ℝ \land B + D < A + D \land A + D < C + D) \leftrightarrow (A \in ℝ \land B < A \land A < C))$
12	2 4	readdcld	$⊢ φ \to B + D \in ℝ$
13	12	rexrd	$⊢ φ \to B + D \in ℝ^{*}$
14	3 4	readdcld	$⊢ φ \to C + D \in ℝ$
15	14	rexrd	$⊢ φ \to C + D \in ℝ^{*}$
16		elioo2	$⊢ (B + D \in ℝ^{} \land C + D \in ℝ^{}) \to (A + D \in (B + D, C + D) \leftrightarrow (A + D \in ℝ \land B + D < A + D \land A + D < C + D))$
17	13 15 16	syl2anc	$⊢ φ \to (A + D \in (B + D, C + D) \leftrightarrow (A + D \in ℝ \land B + D < A + D \land A + D < C + D))$
18	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
19	3	rexrd	$⊢ φ \to C \in ℝ^{*}$
20		elioo2	$⊢ (B \in ℝ^{} \land C \in ℝ^{}) \to (A \in (B, C) \leftrightarrow (A \in ℝ \land B < A \land A < C))$
21	18 19 20	syl2anc	$⊢ φ \to (A \in (B, C) \leftrightarrow (A \in ℝ \land B < A \land A < C))$
22	11 17 21	3bitr4rd	$⊢ φ \to (A \in (B, C) \leftrightarrow A + D \in (B + D, C + D))$

Metamath Proof Explorer