# Mathematica not honoring the distributive property of multiplication?

Bug introduced in 9.0 or earlier and fixed in 10.2

Reduce[
ForAll[
{multiplicant, summandA, summandB},
Element[{multiplicant, summandA, summandB}, Reals],
multiplicant*summandA - multiplicant*summandB == multiplicant*(summandA - summandB)]]

True


Duh. So obvious.

Well, it seems it's not obvious enough for Mathematica. See:

    Multiplicant[x_] := 1/((1 + x^2)*(2 + x^2))

SummandA[x_] := 2*x*(2 + x^2)*Log[2 + x^2]

SummandB[x_] := 2*x*(1 + x^2)*Log[1 + x^2]

Reduce[ForAll[
x, Element[x, Reals],
Multiplicant[x]*SummandA[x] - Multiplicant[x]*SummandB[x] ==
Multiplicant[x]*(SummandA[x] - SummandB[x])]]

False


WHAAAT...?!?!

By the law of the distribution of multiplication over addition the correct result of Out[5] should be True.

Or, the other possibility is that my brain got Shrouded in the Shadows of Shades and thus is unable to work properly.

Or, the other other possibility is that I simply cannot use Mma properly and the above sample is alimented with some kind of PEBKAC.

Could you very kindly help me figure out which one of the above three ideas is correct?

• This is very peculiar behavior, which I can reproduce on 10.0.2 on a Mac. It's especially weird since FullSimplify[ ExpandAll[ Multiplicant[x]*SummandA[x] - Multiplicant[x]*SummandB[x] - Multiplicant[x]*(SummandA[x] - SummandB[x])]] yields 0 (even without the assumption that x is in Reals). Commented Mar 4, 2015 at 22:07
It is a bug in Reduce.
It affects cases when the input contains a univariate equation f==g inside the ForAll quantifier, f-g is not an explicit polynomial, and Together[f-g] is zero.