Theorem eliooshift

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

	Ref	Expression
Hypotheses	eliooshift.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	eliooshift.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	eliooshift.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	eliooshift.d	⊢ ( 𝜑 → 𝐷 ∈ ℝ )
Assertion	eliooshift	⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐵 (,) 𝐶 ) ↔ ( 𝐴 + 𝐷 ) ∈ ( ( 𝐵 + 𝐷 ) (,) ( 𝐶 + 𝐷 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		eliooshift.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		eliooshift.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		eliooshift.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4		eliooshift.d	⊢ ( 𝜑 → 𝐷 ∈ ℝ )
5	1 4	readdcld	⊢ ( 𝜑 → ( 𝐴 + 𝐷 ) ∈ ℝ )
6	5 1	2thd	⊢ ( 𝜑 → ( ( 𝐴 + 𝐷 ) ∈ ℝ ↔ 𝐴 ∈ ℝ ) )
7	2 1 4	ltadd1d	⊢ ( 𝜑 → ( 𝐵 < 𝐴 ↔ ( 𝐵 + 𝐷 ) < ( 𝐴 + 𝐷 ) ) )
8	7	bicomd	⊢ ( 𝜑 → ( ( 𝐵 + 𝐷 ) < ( 𝐴 + 𝐷 ) ↔ 𝐵 < 𝐴 ) )
9	1 3 4	ltadd1d	⊢ ( 𝜑 → ( 𝐴 < 𝐶 ↔ ( 𝐴 + 𝐷 ) < ( 𝐶 + 𝐷 ) ) )
10	9	bicomd	⊢ ( 𝜑 → ( ( 𝐴 + 𝐷 ) < ( 𝐶 + 𝐷 ) ↔ 𝐴 < 𝐶 ) )
11	6 8 10	3anbi123d	⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐷 ) ∈ ℝ ∧ ( 𝐵 + 𝐷 ) < ( 𝐴 + 𝐷 ) ∧ ( 𝐴 + 𝐷 ) < ( 𝐶 + 𝐷 ) ) ↔ ( 𝐴 ∈ ℝ ∧ 𝐵 < 𝐴 ∧ 𝐴 < 𝐶 ) ) )
12	2 4	readdcld	⊢ ( 𝜑 → ( 𝐵 + 𝐷 ) ∈ ℝ )
13	12	rexrd	⊢ ( 𝜑 → ( 𝐵 + 𝐷 ) ∈ ℝ* )
14	3 4	readdcld	⊢ ( 𝜑 → ( 𝐶 + 𝐷 ) ∈ ℝ )
15	14	rexrd	⊢ ( 𝜑 → ( 𝐶 + 𝐷 ) ∈ ℝ* )
16		elioo2	⊢ ( ( ( 𝐵 + 𝐷 ) ∈ ℝ* ∧ ( 𝐶 + 𝐷 ) ∈ ℝ* ) → ( ( 𝐴 + 𝐷 ) ∈ ( ( 𝐵 + 𝐷 ) (,) ( 𝐶 + 𝐷 ) ) ↔ ( ( 𝐴 + 𝐷 ) ∈ ℝ ∧ ( 𝐵 + 𝐷 ) < ( 𝐴 + 𝐷 ) ∧ ( 𝐴 + 𝐷 ) < ( 𝐶 + 𝐷 ) ) ) )
17	13 15 16	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 + 𝐷 ) ∈ ( ( 𝐵 + 𝐷 ) (,) ( 𝐶 + 𝐷 ) ) ↔ ( ( 𝐴 + 𝐷 ) ∈ ℝ ∧ ( 𝐵 + 𝐷 ) < ( 𝐴 + 𝐷 ) ∧ ( 𝐴 + 𝐷 ) < ( 𝐶 + 𝐷 ) ) ) )
18	2	rexrd	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
19	3	rexrd	⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
20		elioo2	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝐴 ∈ ( 𝐵 (,) 𝐶 ) ↔ ( 𝐴 ∈ ℝ ∧ 𝐵 < 𝐴 ∧ 𝐴 < 𝐶 ) ) )
21	18 19 20	syl2anc	⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐵 (,) 𝐶 ) ↔ ( 𝐴 ∈ ℝ ∧ 𝐵 < 𝐴 ∧ 𝐴 < 𝐶 ) ) )
22	11 17 21	3bitr4rd	⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐵 (,) 𝐶 ) ↔ ( 𝐴 + 𝐷 ) ∈ ( ( 𝐵 + 𝐷 ) (,) ( 𝐶 + 𝐷 ) ) ) )