Pardon my curiosity, but I'm wondering how Wolfram calculates
FullSimplify[x == q Quotient[x, q] + Mod[x, q]].
I tried Trace and the TraceOriginal->True option, but I still don't get it. Does Wolfram know it's True, or does it apply some transformation rules to get True?
This behavior is documented in the "Properties & Relations" section of https://reference.wolfram.com/language/ref/Quotient.html (3rd example therein).
Rather, from the examples given there, we should conclude that the result is derived from theory rather than computation.
Got it. Thanks!!! I mistakenly thought that Wolfram computes in much the same way I write a sequence of commands, just along all paths at once, and selects the ones that get closest to the result. It turns out that applying a built-in function is not so easy to detect, much less see the entire computation process.
Using Reduce I get the message that it is using FunctionExpand:
Reduce
FunctionExpand
Reduce[x == q Quotient[x, q] + Mod[x, q]]
In fact FunctionExpand translates the expression into Floor objects:
Floor
FunctionExpand[q Quotient[x, q]] FunctionExpand[Mod[x, q]]
I tried that too, but I didn't detect those transformations. How did you find them?
