This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐵 (,) 𝐶 ) ↔ ( 𝐴 + 𝐷 ) ∈ ( ( 𝐵 + 𝐷 ) (,) ( 𝐶 + 𝐷 ) ) ) )