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∈AB↔X+R∈CD

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∈AB↔X∈ℝ∧A≤X∧X≤B
20 19 adantr ⊢A∈ℝ∧B∈ℝ∧X∈ℝ∧R∈ℝ→X∈AB↔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∈CD↔X+R∈ℝ∧C≤X+R∧X+R≤D
26 22 24 25 syl2an ⊢A∈ℝ∧R∈ℝ∧B∈ℝ∧R∈ℝ→X+R∈CD↔X+R∈ℝ∧C≤X+R∧X+R≤D
27 26 anandirs ⊢A∈ℝ∧B∈ℝ∧R∈ℝ→X+R∈CD↔X+R∈ℝ∧C≤X+R∧X+R≤D
28 27 adantrl ⊢A∈ℝ∧B∈ℝ∧X∈ℝ∧R∈ℝ→X+R∈CD↔X+R∈ℝ∧C≤X+R∧X+R≤D
29 18 20 28 3bitr4d ⊢A∈ℝ∧B∈ℝ∧X∈ℝ∧R∈ℝ→X∈AB↔X+R∈CD