3
$\begingroup$

I have to solve the following problem concerning a system of inequalities:

Distinguish two groups of real variables: the first composed by the following 15 real variables

Cx, Ox, alpha, Bx,By, Dx,Dy, ax, ay, bx, by, cx, cy, dx, dy

and the second composed by the following 12 real variables:

dBx, dBy, dDx, dDy, dax, day, dbx, dby, dcx, dcy, ddx, ddy

The variables in the first group can assume real values subjected to the following constrains:

Cx > 0, 
0 < Ox < Cx, 
alpha > 0, 
Bx > Ox, By == alpha (Bx - Ox), 
Dx < Ox, 
Dy == alpha (Dx - Ox), 
0 < ay < By, 
(Bx/By) ay < ax < (ay/alpha) + Ox, 
0 < by < By, 
(by/alpha) + Ox < bx < ((Bx - Cx)/By) by + Cx, 
Dy < cy < 0, 
cy/alpha + Ox < cx < ((Dx - Cx)/Dy) cy + Cx, 
Dy < dy < 0, 
(Dx/Dy) dy < dx < dy/alpha + Ox

For each possible 13-nple of values that the variables in the first group can assume, consider the following system of equalities and inequalities:

(Bx - Dx) dBx + (By - Dy) dBy + (Dx - Bx) dDx + (Dy - By) dBy == 0, 
ax*dax + ay*day <= 0, 
(ax - Bx) dax + (ay - By) day + (Bx - ax) dBx + (By - ay) dBy <= 0, 
(Bx - bx) dBx + (By - by) dBy + (bx - Bx) dbx + (by - By) dby <= 0, 
(bx - Cx) dbx + by*dby <= 0, 
(cx - Cx) dcx + cy*dcy <= 0, 
(cx - Dx) dcx + (cy - Dy) dcy + (Dx - cx) dDx + (Dy - cy) dDy <= 0, 
(Dx - dx) dDx + (Dy - dy) dDy + (dx - Dx) ddx + (dy - Dy) ddy <= 0, 
dx*ddx + dy*ddy <= 0, 
(ax - cx) dax + (ay - cy) day + (cx - ax) dcx + (cy - ay) dcy <= 0, 
(bx - dx) dbx + (by - dy) dby + (dx - bx) ddx + (dy - by) ddy <= 0, 
(ax - bx) dax + (ay - by) day + (bx - ax) dbx + (by - ay) dby <= 0, 
(ax - dx) dax + (ay - dy) day + (dx - ax) ddx + (dy - ay) ddy <= 0, 
(bx - cx) dbx + (by - cy) dby + (cx - bx) dcx + (cy - by) dcy <= 0, 
(cx - dx) dcx + (cy - dy) dcy + (dx - cx) ddx + (dy - cy) ddy <= 0

I have to verify if the following claim is true:

Claim: for each possible 13-nple of values that the variables in the first group can assume, the corresponding system of equalities and inequalities is satisfied if and only if all the variables in the second group are equal to zero.

But I have no clue on how to proceed: I only tried to use Solve, but with no success.. Do you have any suggestions?

$\endgroup$

closed as off-topic by MarcoB, m_goldberg, José Antonio Díaz Navas, Coolwater, Sektor Apr 25 '18 at 21:08

This question appears to be off-topic. The users who voted to close gave this specific reason:

  • "The question is out of scope for this site. The answer to this question requires either advice from Wolfram support or the services of a professional consultant." – MarcoB, m_goldberg, José Antonio Díaz Navas, Coolwater, Sektor
If this question can be reworded to fit the rules in the help center, please edit the question.

  • $\begingroup$ your first set of conditions contains a By which is not in either list. $\endgroup$ – george2079 May 16 '17 at 14:59
  • $\begingroup$ yes, sorry, I've added it $\endgroup$ – user294185 May 16 '17 at 16:59
  • $\begingroup$ You can use FindInstance to get a particular solution to the first set of conditions, plug that to the second set and let Reduce go at it. I don't have the patience to see how long that takes..and of course that doesn't prove the general assertion anyway. ( In principle you can let Reduce work on the whole thing, but it is doubtful that will work in any reasonable time ) $\endgroup$ – george2079 May 16 '17 at 17:11
  • $\begingroup$ Yes, that's the point: Reduce won't solve the whole thing in a reasonable time. Isn't there any better way to do it? $\endgroup$ – user294185 May 16 '17 at 17:20