Metamath Proof Explorer


Theorem icccntr

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

Ref Expression
Hypotheses icccntr.1 A R = C
icccntr.2 B R = D
Assertion icccntr A B X R + X A B X R C D

Proof

Step Hyp Ref Expression
1 icccntr.1 A R = C
2 icccntr.2 B R = D
3 simpl X R + X
4 rerpdivcl X R + X R
5 3 4 2thd X R + X X R
6 5 adantl A B X R + X X R
7 elrp R + R 0 < R
8 lediv1 A X R 0 < R A X A R X R
9 7 8 syl3an3b A X R + A X A R X R
10 9 3expb A X R + A X A R X R
11 10 adantlr A B X R + A X A R X R
12 1 breq1i A R X R C X R
13 11 12 bitrdi A B X R + A X C X R
14 lediv1 X B R 0 < R X B X R B R
15 7 14 syl3an3b X B R + X B X R B R
16 15 3expb X B R + X B X R B R
17 16 an12s B X R + X B X R B R
18 17 adantll A B X R + X B X R B R
19 2 breq2i X R B R X R D
20 18 19 bitrdi A B X R + X B X R D
21 6 13 20 3anbi123d A B X R + X A X X B X R C X R X R D
22 elicc2 A B X A B X A X X B
23 22 adantr A B X R + X A B X A X X B
24 rerpdivcl A R + A R
25 1 24 eqeltrrid A R + C
26 rerpdivcl B R + B R
27 2 26 eqeltrrid B R + D
28 elicc2 C D X R C D X R C X R X R D
29 25 27 28 syl2an A R + B R + X R C D X R C X R X R D
30 29 anandirs A B R + X R C D X R C X R X R D
31 30 adantrl A B X R + X R C D X R C X R X R D
32 21 23 31 3bitr4d A B X R + X A B X R C D