Metamath Proof Explorer

Theorem iccshftl

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

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

Proof

Step Hyp Ref Expression
1 iccshftl.1 ⊢ A − R = C
2 iccshftl.2 ⊢ B − R = D
3 simpl ⊢ X ∈ ℝ ∧ R ∈ ℝ → X ∈ ℝ
4 resubcl ⊢ X ∈ ℝ ∧ R ∈ ℝ → X − R ∈ ℝ
5 3 4 2thd ⊢ X ∈ ℝ ∧ R ∈ ℝ → X ∈ ℝ ↔ X − R ∈ ℝ
6 5 adantl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ X ∈ ℝ ∧ R ∈ ℝ → X ∈ ℝ ↔ X − R ∈ ℝ
7 lesub1 ⊢ 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 lesub1 ⊢ 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 resubcl ⊢ A ∈ ℝ ∧ R ∈ ℝ → A − R ∈ ℝ
22 1 21 eqeltrrid ⊢ A ∈ ℝ ∧ R ∈ ℝ → C ∈ ℝ
23 resubcl ⊢ 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