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

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∈AB↔X∈ℝ∧A≤X∧X≤B
20 19 adantr ⊢A∈ℝ∧B∈ℝ∧X∈ℝ∧R∈ℝ→X∈AB↔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∈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