Metamath Proof Explorer


Theorem iccdili

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

Ref Expression
Hypotheses iccdili.1 A
iccdili.2 B
iccdili.3 R +
iccdili.4 A R = C
iccdili.5 B R = D
Assertion iccdili X A B X R C D

Proof

Step Hyp Ref Expression
1 iccdili.1 A
2 iccdili.2 B
3 iccdili.3 R +
4 iccdili.4 A R = C
5 iccdili.5 B R = D
6 iccssre A B A B
7 1 2 6 mp2an A B
8 7 sseli X A B X
9 4 5 iccdil A B X R + X A B X R C D
10 1 2 9 mpanl12 X R + X A B X R C D
11 3 10 mpan2 X X A B X R C D
12 11 biimpd X X A B X R C D
13 8 12 mpcom X A B X R C D