2
$\begingroup$

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.

  • 2
    See http://en.wikipedia.org/wiki/Modular_arithmetic.2012-08-09
  • 0
    @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.)2012-08-09
  • 0
    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.2012-08-09
  • 0
    @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. :)2012-08-09
  • 0
    @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](http://en.wikipedia.org/wiki/Modular_multiplicative_inverse).2012-08-11

2 Answers 2

3

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)\:$

  • 0
    Thanks. It seems obvious now in hindsight.2012-08-09
  • 0
    @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.2012-08-09
4

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.

  • 0
    +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.2012-08-09