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.