[Algebra] Proving equations involving modulo functions.

[ellipsis]

I would like to know some general properties of the modulo (remainder) function that I can use to rewrite expressions. For example, say we wanted to prove the following by rewriting the right-hand-side:

$$ \Big{\lfloor} \frac{n}{d} \Big{\rfloor} = \frac{n - n \pmod d}{d} $$

I have no idea how to prove this statement formally. Intuitively, $n \pmod d$ is the remainder of whatever $\big{\lfloor} \frac{n}{d} \big{\rfloor}$ is, and therefore

$$ n \pmod d = n - d \Big{\lfloor} \frac{n}{d} \Big{\rfloor}$$

Which, when we insert it into the right-hand side of what I'm trying to prove, results in:

$$ \frac{n - (n - d \big{\lfloor} \frac{n}{d} \big{\rfloor})}{d} $$

Which, thankfully, boils down to:

$$ \Big{\lfloor} \frac{n}{d} \Big{\rfloor} $$

What I want to know is: How do I formalize the beginning of this proof? Is there some general property or definition of the modulo function which I can invoke to justify that step?

 

[RUber]

a = n mod d is defined as a number between 0 and d such that there exists an integer c such that n = cd+a.
When you take d*floor(n/d), you are essentially saying that floor(n/d) = c. That is, there is no integer larger than c such that cd is less than or equal to n.