I need to show that the following expression, $$a^3b-a^3c+a^3z+a^3x+a^3y-a^2bx+a^2by+a^2cx-a^2cy-a^2zx+a^2zy-a^2x^2+a^2y^2-abcz-abcx-aczx-acx^2+b^2c^2+2bc^2x+c^2x^2-b^2c-2bcx-cx^2,$$
is positive
given that:
$1.$ $\ a,b,c,x,y,z$ are positive real numbers
$2. \ \ a>b+x$
$3. \ \ c<b+y$
I know a priori that the expression is indeed positive, but I do not know how to show it, or how to use Maple to do it?
Specifically, how can I use Maple to partially factorize the expression in terms of the expressions $a-b-x$ and $c-b-y$?
Thanks for any help.
I don't know how to use Maple for this. I'll explain how to do this kind of thing by hand, the way I answered your previous question of this type.
What we want is to rewrite the given expression in terms of sums of products of things whose signs we know, like $a-b-x$ and $b+y-c$. So let's look at the first term: $$ a^3 b $$ This has an $a$ in it, so maybe it comes from a term with a factor of $(a-b-x)$. Since the term we're looking at is $a^2b\cdot a$, we now think that maybe $$ a^2b (a-b-x) $$ occurs in our final expression. If so, then we would expect all of the terms $$ a^3b - a^2b^2 - a^2bx $$ to be in our initial expression. We do have $a^3b$ and $-a^2bx$, but we don't see $-a^2b^2$.
Two ways to proceed at this point: we could either abandon the idea of getting $a^3b$ from $a^2b(a-b-x)$, and maybe try instead to get it from $a^3(b+y-c)$, or we could just force it. I'll try forcing it. We don't see $-a^2b^2$, so let's introduce it: add $$ {}+a^2b^2 - a^2b^2 $$ at the end of your expression. Then we have $a^3b - a^2b^2 - a^2bx$, and we can rewrite the whole expression as $$ \require{cancel} \cancel{a^3b} - a^3 c + a^3 z + a^3 x + a^3 y - \cancel{a^2bx} + a^2 b y + a^2 c x - a^2 c y - a^2 z x + a^2 z y - a^2 x^2 + a^2 y^2 \\ - a b c z - a b c x - a c z x - a c x^2 + b^2 c^2 + 2 b c^2 x + c^2 x^2 - b^2 c - 2 b c x - c x^2 \\ + a^2 b^2 - \cancel{a^2b^2} + \underbrace{a^2b(a-b-x)}_{\text{positive}} $$
So far so good. Move on to the next term: it's $-a^3c$. With the negative in front, we don't want to get it from $a-b-x$, because then we'd produce a term like $-a^2(a-b-x)$, which is negative, and who knows whether we'll be able to control it with something else later. But we could get $-a^3c$ from $a^3(b+y-c)$ instead, and that's positive. This would call for finding $a^3b$ and $a^3y$. We have $a^3y$, but not $a^3 b$, since we used it up in the previous step. So now maybe we regret making that previous step, and think we should go back and try the other option.
Doing that, we end up with $$ \cancel{a^3b} - \cancel{a^3 c} + a^3 z + a^3 x + \cancel{a^3 y} - a^2bx + a^2 b y + a^2 c x - a^2 c y - a^2 z x + a^2 z y - a^2 x^2 + a^2 y^2 \\ - a b c z - a b c x - a c z x - a c x^2 + b^2 c^2 + 2 b c^2 x + c^2 x^2 - b^2 c - 2 b c x - c x^2 \\ + a^3(b+y-c) $$
Now maybe look at $-a^2bx$, which (again because of the negative) we probably want to get from $a^2x(a-b-x)$ or from $a^2b(a-b-x)$. Let's try the first. Then we need $a^3x$ and $-a^2x^2$; we have both. So we rewrite as $$ \cancel{a^3b} - \cancel{a^3 c} + a^3 z + \cancel{a^3 x} + \cancel{a^3 y} - \cancel{a^2bx} + a^2 b y + a^2 c x - a^2 c y - a^2 z x + a^2 z y - \cancel{a^2 x^2} + a^2 y^2 \\ - a b c z - a b c x - a c z x - a c x^2 + b^2 c^2 + 2 b c^2 x + c^2 x^2 - b^2 c - 2 b c x - c x^2 \\ + a^3(b+y-c) + a^2x(a-b-x) $$
And so on. Combining this kind of semi-systematic fiddling with looking for familiar factorizations like $-c(b+c)^2$ for the last three terms, you'll group everything into terms whose signs you can figure out. I ended up with one term being like $c(c-1)$ times something positive, and that led to the counterexample in my comment.