Metamath Proof Explorer

Theorem iccshftr

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

Ref Expression
Hypotheses iccshftr.1 ⊢ A + R = C
iccshftr.2 ⊢ B + R = D
Assertion iccshftr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ X ∈ ℝ ∧ R ∈ ℝ → X ∈ A B ↔ X + R ∈ C D

Proof

Step Hyp Ref Expression
1 iccshftr.1 ⊢ A + R = C
2 iccshftr.2 ⊢ B + R = D
3 simpl ⊢ X ∈ ℝ ∧ R ∈ ℝ → X ∈ ℝ
4 readdcl ⊢ X ∈ ℝ ∧ R ∈ ℝ → X + R ∈ ℝ
5 3 4 2thd ⊢ X ∈ ℝ ∧ R ∈ ℝ → X ∈ ℝ ↔ X + R ∈ ℝ
6 5 adantl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ X ∈ ℝ ∧ R ∈ ℝ → X ∈ ℝ ↔ X + R ∈ ℝ
7 leadd1 ⊢ A ∈ ℝ ∧ X ∈ ℝ ∧ R ∈ ℝ → A ≤ X ↔ A + R ≤ X + R
8 7 3expb ⊢ A ∈ ℝ ∧ X ∈ ℝ ∧ R ∈ ℝ → A ≤ X ↔ A + R ≤ X + R
9 8 adantlr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ X ∈ ℝ ∧ R ∈ ℝ → A ≤ X ↔ A + R ≤ X + R
10 1 breq1i ⊢ A + R ≤ X + R ↔ C ≤ X + R
11 9 10 bitrdi ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ X ∈ ℝ ∧ R ∈ ℝ → A ≤ X ↔ C ≤ X + R
12 leadd1 ⊢ X ∈ ℝ ∧ B ∈ ℝ ∧ R ∈ ℝ → X ≤ B ↔ X + R ≤ B + R
13 12 3expb ⊢ X ∈ ℝ ∧ B ∈ ℝ ∧ R ∈ ℝ → X ≤ B ↔ X + R ≤ B + R
14 13 an12s ⊢ B ∈ ℝ ∧ X ∈ ℝ ∧ R ∈ ℝ → X ≤ B ↔ X + R ≤ B + R
15 14 adantll ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ X ∈ ℝ ∧ R ∈ ℝ → X ≤ B ↔ X + R ≤ B + R
16 2 breq2i ⊢ X + R ≤ B + R ↔ X + R ≤ D
17 15 16 bitrdi ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ X ∈ ℝ ∧ R ∈ ℝ → X ≤ B ↔ X + R ≤ D
18 6 11 17 3anbi123d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ X ∈ ℝ ∧ R ∈ ℝ → X ∈ ℝ ∧ A ≤ X ∧ X ≤ B ↔ X + R ∈ ℝ ∧ C ≤ X + R ∧ X + R ≤ D
19 elicc2 ⊢ A ∈ ℝ ∧ B ∈ ℝ → X ∈ A B ↔ X ∈ ℝ ∧ A ≤ X ∧ X ≤ B
20 19 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ X ∈ ℝ ∧ R ∈ ℝ → X ∈ A B ↔ X ∈ ℝ ∧ A ≤ X ∧ X ≤ B
21 readdcl ⊢ A ∈ ℝ ∧ R ∈ ℝ → A + R ∈ ℝ
22 1 21 eqeltrrid ⊢ A ∈ ℝ ∧ R ∈ ℝ → C ∈ ℝ
23 readdcl ⊢ B ∈ ℝ ∧ R ∈ ℝ → B + R ∈ ℝ
24 2 23 eqeltrrid ⊢ B ∈ ℝ ∧ R ∈ ℝ → D ∈ ℝ
25 elicc2 ⊢ C ∈ ℝ ∧ D ∈ ℝ → X + R ∈ C D ↔ X + R ∈ ℝ ∧ C ≤ X + R ∧ X + R ≤ D
26 22 24 25 syl2an ⊢ A ∈ ℝ ∧ R ∈ ℝ ∧ B ∈ ℝ ∧ R ∈ ℝ → X + R ∈ C D ↔ X + R ∈ ℝ ∧ C ≤ X + R ∧ X + R ≤ D
27 26 anandirs ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ R ∈ ℝ → X + R ∈ C D ↔ X + R ∈ ℝ ∧ C ≤ X + R ∧ X + R ≤ D
28 27 adantrl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ X ∈ ℝ ∧ R ∈ ℝ → X + R ∈ C D ↔ X + R ∈ ℝ ∧ C ≤ X + R ∧ X + R ≤ D
29 18 20 28 3bitr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ X ∈ ℝ ∧ R ∈ ℝ → X ∈ A B ↔ X + R ∈ C D