Checking inequalities: How can $x>0,y>0$ yet $x+y$ indeterminate?

Question

I have the following:

$Assumptions = {0 < Ijm1 < Ij < Ijp1 < 1, bpjm1 < 0, bpj < 0, 
bpjp1 < 0, Ijm1 \[Element] Reals, Ij \[Element] Reals, 
Ijp1 \[Element] Reals, bpjm1 \[Element] Reals, bjp \[Element] Reals,
bpjp1 \[Element] Reals};

x = (1 - bpjp1 Ijp1 + bpjp1 Ijp1^2) ;
y = bpj (Ij - Ijm1) (-1 + Ij (1 + bpjp1 (-1 + Ijp1)) - 
bpjp1 (-1 + Ijp1) Ijp1);

When checking inequalities I get

In[243]:= Simplify[x > 0]
Out[243]= True

In[244]:= Simplify[y > 0]
Out[244]= True

but

In[245]:= Simplify[x + y > 0]  
Out[245]= 
1 + bpjp1 (-1 + Ijp1) Ijp1 + 
bpj (Ij - Ijm1) (-1 + Ij (1 + bpjp1 (-1 + Ijp1)) - 
bpjp1 (-1 + Ijp1) Ijp1) > 0

Why?

Answer 1

The assumptions mechanism used by Simplify has a bound on the number of variables in a system of nonlinear inequalities. If the number of variables exceeds the bound, the assumption mechanism does not attempt to decide whether the system has solutions. (Simplify proves that an inequality follows from the assumptions by showing that assumptions && Not[inequality] has no solutions.) The default value of the bound is 4, but it can be changed using a system option.

SetSystemOptions["SimplificationOptions"->{"AssumptionsMaxNonlinearVariables"->5}];

Simplify[x + y > 0]
True

Answer 2

This is not an answer, but here's some analysis of the issue which didn't fit in a comment.

First, let us rewrite your assumptions in a slightly different form:

asmp = And @@ {0 < Ijm1 < Ij < Ijp1 < 1, bpjm1 < 0, bpj < 0, 
    bpjp1 < 0, Ijm1 ∈ Reals, Ij ∈ Reals, 
    Ijp1 ∈ Reals, bpjm1 ∈ Reals, 
    bjp ∈ Reals, bpjp1 ∈ Reals};

Now let's play with Reduce:

Reduce[Implies[asmp, x > 0], Reals]
(* True *)

Reduce[Implies[asmp, y > 0], Reals]
(* True *)

All good so far. But what about this?

res = Reduce[Implies[asmp, x + y > 0], Reals]
(* Ij < 
  1 || (Ij == 
    1 && (Ijm1 <= 
      0 || (0 < Ijm1 < 1 && (Ijp1 < 1 || Ijp1 == 1 || Ijp1 > 1)) || 
     Ijm1 >= 1)) || Ij > 1 *)

What is strange about this result is that:

Reduce[Implies[asmp, res], Reals]
(* True *)

And also that

Reduce[Implies[Reduce[asmp], x + y > 0], Reals]
(* True *)

Also that it contains things like Ijp1 < 1 || Ijp1 == 1 || Ijp1 > 1, which are obviously True and that it contains Ijm1 <= 0 and Ij > 1, which contradict asmp so should be dropped.

Somehow Reduce doesn't seem to finish its job.