How can I prove that two remainders are equivalent?

I have the following mathematical statement that I believe to be true, but I need to prove that it is:

(1) rem(x·y, z) = rem(x·rem(y, z), z)


Using the definition that:

rem(a, b) = a - b·div(a, b)


I can show that this is equivalent to proving:

(2) div(x·y, z) = x·div(y, z) + div(x·rem(y, z), z)


So being able to prove this would also work. In fact, proving the last equality (2) is what got me to the first equality (1). The primary reason for wanting to prove this is that I have a specification requiring me to calculate div(x·y, z) using 32-bit integers, but there are cases where x·y might exceed $2^{32} - 1$ but where div(x·y, z), x·div(y, z), and div(x·rem(y, z), z) will not.

-
– joriki Aug 9 '12 at 19:29
@joriki: If I understand that, then because y is congruent modulo z to mod(y, z), then I can replace the mod(y, z) in mod(x·mod(y, z), z) with y, giving me mod(x·y, z), which satisfies (1) when x·y, y, and z are non-negative. (In my particular problem x and z are always non-negative, but y can be positive or negative.) – Ben Hocking Aug 9 '12 at 19:44
I hadn't given thought to the possibility of $y$ being negative. I like to think of remainders $\bmod n$ always lying in $[0,n-1]$; then this sort of problem doesn't come up; but since your definition of rem (a,b) allows for negative remainders, I guess you do have to worry about that. – joriki Aug 9 '12 at 22:35
@joriki: The good news is that if all are non-negative it works, and with x, z positive and y negative, rem(y, z) = mod(y, z) - z and rem(x·rem(y, z)) = rem(x·(mod(y, z) - z)) = mod(x·(mod(y, z) - z)) - z = mod(y, z) - z. QED. :) – Ben Hocking Aug 9 '12 at 22:49
@BenHocking it's also worth noting that the converse $xy \equiv x\bar{y} \pmod{z} \implies y \equiv \bar{y} \pmod{z}$ is true iff $x$ and $z$ are coprime. See modular multiplicative inverse on WP. – user2468 Aug 11 '12 at 16:00

Hint $\rm\ mod\ z\!:\ y\equiv \bar y\:\Rightarrow\: xy\equiv x\bar y,\:$ so $\rm\: rem(xy,z) = rem(x\bar y,z).\:$ Now let $\rm\:\bar y = rem(y,z)\:$

-
Thanks. It seems obvious now in hindsight. – Ben Hocking Aug 9 '12 at 19:46
@Ben That's good that it seems obvious, since it shows that you have grokked modular (congruence) arithmetic - which serves to remove the obfuscation from these type of problems by working generally with more abstract congruence classes, till the end, when one specializes to particular class rep's, such as the least natural rep, as above. – Bill Dubuque Aug 9 '12 at 19:51

Note that rem(_,z) is invariant with respect to addition or subtraction of multiples of z in the first argument, so we have (using the "division algorithm" for y=div(y,z)z+rem(y,z)):

$$\rm \begin{array}{c l}rem(x\,\mathbf{y},z) & \rm = rem(x\,(\mathbf{div(y,z)\,z+rem(y,z)}),z) \\ & \rm = rem(\mathbf{(x \,div(y,z))}z+x\,rem(y,z),z) \\ & \rm =rem(x\,rem(y,z),z). \end{array}$$

This is the "assembly language" derivation underlying the modular arithmetic.

-
+1 Yes, you've essentially "inlined" what I call-by-name (i.e. invoke as a lemma). But it is instructive to see it both ways, since it shows how the abstraction (congruence arithmetic) serves to simplify matters. – Bill Dubuque Aug 9 '12 at 19:54