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