Strange behaviour of Reduce for Mod[x,1]

Question

For every integer $x$ the equation Mod[x, 1] == 0 holds. While

Simplify[Mod[x, 1] == 0, Element[x,Integers]] 

gives True,

Reduce[Mod[x, 1] == 0, x, Integers] 

gives False. Why?

Answer 1

Reduce works fine for a slightly more sophisticated expression, e.g. :

Reduce[ ForAll[ x, x ∈ Integers, Mod[ x, 1] == 0], x]

True

however there is a bug in Solve :

Solve[ Mod[x, 1] == 0, x, Integers]

{}

therefore it is not surprising we have an analogical issue in Reduce :

Reduce[ Mod[x, 1] == 0, x, Integers] 

False 

Seemingly there has not been much clamor therefore it has not been a high priority to improve it.

One can work around these problems :

Reduce[ Mod[ a x, a] == 0 && a == 1, x, Integers]

C[1] ∈ Integers && a == 1 && x == C[1]

or simply

Reduce[ Mod[ x, 1] == a, x, Integers]

C[1] ∈ Integers && a == 0 && x == C[1]

Solve[ Mod[ x, 1] == a, x, Integers]

{{x -> ConditionalExpression[C[1], C[1] ∈ Integers && a == 0]}}

Edit

The above problems with Reduce and Solve were found in Mathematica 8. Before there had been :

ver. 7

Solve[ Mod[x, 1] == 0, x, Integers]

Solve::ifun: Inverse functions are being used by Solve, so some solutions may not
be found; use Reduce for complete solution information. >> 

{{x -> InverseFunction[Mod, 1, 2][0, 1]}}

Reduce[ Mod[x, 1] == 0, x, Integers]

False

Now these bugs have been fixed :

ver. 9

Solve[ Mod[x, 1] == 0, x, Integers]

{{x -> ConditionalExpression[C[1], C[1] ∈ Integers]}}

Reduce[ Mod[x, 1] == 0, x, Integers]

C[1] ∈ Integers && x == C[1]