Resolving a logical statement

I would like to test whether f[n] > 0 and f[n + 1] > 0 implies f[n + 2] > 0. This is what I tried:

f[n] == n*f[n - 2] + f[n - 1];
Resolve[ForAll[n, Implies[n > 0 && f[n - 2] > 0 && f[n - 1] > 0, f[n] > 0]], Reals]


I was expecting output True, but Mathematica doesn't do anything with this. Any idea what I need to do to have this work the way I would expect?

• @m_goldberg Basically because the number of variables I'm going to use is not constant, but I see I can substitute y[i] and it's no problem. But now I have a different problem with this statement. – user31953 Mar 5 '15 at 15:10

You should formulate your problem in its simplest form.

Resolve[ForAll[{n, a, b}, n > 0 && a > 0 && b > 0, n a + b > 0]]

True


You can do it with the complications you introduce into your question.

Resolve[ForAll[{n, a, b}, n > 0 && a > 0 && b > 0, n a + b > 0] /.
{a -> f[n - 2], b -> f[n - 1]}]

True


But why bother? They are irrelevant.

• but I do want to use the recursively defined function – user31953 Feb 25 '15 at 14:44
• @user31953. Why? If the statement is true for arbitrary a and b, it is obviously true in your more restricted case. – m_goldberg Feb 25 '15 at 14:47
• Basically I was just making a mistake because I didn't want to have a fixed number of variable, but I see I can substitute some indexed variables where you have a and b. Now I have a different problem with this same statement mathematica.stackexchange.com/questions/76528/… – user31953 Mar 5 '15 at 15:16