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?