Theorem: Summation over k of Floor of mk+x over n

Let $m, n \in \Z$ such that $n > 0$.
Let $x \in \R$.
Then:
:$\ds \sum_{0 \mathop \le k \mathop < n} \floor {\dfrac {m k + x} n} = \dfrac {\paren {m - 1} \paren {n - 1} } 2 + \dfrac {d - 1} 2 + d \floor {\dfrac x d}$
where:
:$\floor x$ denotes the floor of $x$
:$d$ is the greatest common divisor of $m$ and $n$.

Proof:
By definition of modulo 1:
:$\ds \sum_{0 \mathop \le k \mathop < n} \floor {\dfrac {m k + x} n} = \sum_{0 \mathop \le k \mathop < n} \dfrac {m k + x} n - \sum_{0 \mathop \le k \mathop < n} \fractpart {\dfrac {m k + x} n}$
where $\fractpart y$ in this context denotes the fractional part of $y$.
First we have:
{{begin-eqn}}
{{eqn | l = \sum_{0 \mathop \le k \mathop < n} \dfrac {m k + x} n
      | r = \frac m n \sum_{0 \mathop \le k \mathop < n} k + \sum_{0 \mathop \le k \mathop < n} \dfrac x n
      | c = 
}}
{{eqn | r = \frac m n \frac {n \paren {n - 1} } 2 + n \dfrac x n
      | c = Closed Form for Triangular Numbers
}}
{{eqn | r = \frac {m \paren {n - 1} } 2 + x
      | c = 
}}
{{end-eqn}}
Let $S$ be defined as:
:$\ds S := \sum_{0 \mathop \le k \mathop < n} \fractpart {\dfrac {m k + x} n}$
Thus:
:$(1): \quad \ds \sum_{0 \mathop \le k \mathop < n} \floor {\dfrac {m k + x} n} = \dfrac {m \paren {n - 1} } 2 + x - S$
Let $d = \gcd \set {m, n}$.
Let:
{{begin-eqn}}
{{eqn | l = t
      | r = \frac n d
}}
{{eqn | l = u
      | r = \frac m d
}}
{{eqn | ll= \leadsto
      | l = \frac m n
      | r = \frac u t
      | c = 
}}
{{eqn | ll= \leadsto
      | l = m t
      | r = u n
      | c = 
}}
{{eqn | ll= \leadsto
      | l = u
      | r = \frac {m t} n
      | c = 
}}
{{end-eqn}}
We have that:
{{begin-eqn}}
{{eqn | l = \fractpart {\dfrac {m k + x} n}
      | r = \fractpart {\dfrac {m k + x} n + u}
      | c = {{Defof|Fractional Part}}: $u$ is an integer
}}
{{eqn | r = \fractpart {\dfrac {m k + x} n + \frac {m t} n}
      | c = 
}}
{{eqn | r = \fractpart {\dfrac {m \paren {k + t} + x} n}
      | c = 
}}
{{end-eqn}}
Thus $S$ consists of $d$ copies of the same summation:
{{begin-eqn}}
{{eqn | l = S
      | r = \sum_{0 \mathop \le k \mathop < n} \fractpart {\dfrac {m k + x} n}
      | c = 
}}
{{eqn | r = d \sum_{0 \mathop \le k \mathop < t} \fractpart {\dfrac {m k + x} n}
      | c = 
}}
{{end-eqn}}
and so:
{{begin-eqn}}
{{eqn | l = \sum_{0 \mathop \le k \mathop < t} \fractpart {\dfrac {m k + x} n}
      | r = \sum_{0 \mathop \le k \mathop < t} \fractpart {\dfrac x n + \dfrac {u k} t}
      | c = substituting $\dfrac u t$ for $\dfrac m n$
}}
{{eqn | r = \sum_{0 \mathop \le k \mathop < t} \fractpart {\dfrac {x \bmod d} n + \dfrac k t}
      | c = as $t \perp u$
}}
{{eqn | r = \sum_{0 \mathop \le k \mathop < t} \dfrac {x \bmod d} n + \dfrac k t
      | c = as $\dfrac {x \bmod d} n < \dfrac 1 t$
}}
{{eqn | r = t \dfrac {x \bmod d} n + \frac 1 t \sum_{0 \mathop \le k \mathop < t} k
      | c = 
}}
{{eqn | r = \dfrac {t \paren {x \bmod d} } n + \frac 1 t \frac {t \paren {t - 1} } 2
      | c = Closed Form for Triangular Numbers
}}
{{eqn | r = \dfrac {t \paren {x \bmod d} } n + \frac {t - 1} 2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = S
      | r = d \paren {\dfrac {t \paren {x \bmod d} } n + \frac {t - 1} 2}
      | c = 
}}
{{eqn | r = \dfrac {n \paren {x \bmod d} } n + \frac {n - d} 2
      | c = as $n = d t$
}}
{{eqn | r = x \bmod d + \frac {n - d} 2
      | c = 
}}
{{end-eqn}}
{{explain|Greater detail needed as to why $\ds \sum_{0 \mathop \le k \mathop < t} \fractpart {\dfrac x n + \dfrac {u k} t} {{=}} \sum_{0 \mathop \le k \mathop < t} \fractpart {\dfrac {x \bmod d} n + \dfrac k t}$}}
Thus:
{{begin-eqn}}
{{eqn | l = \sum_{0 \mathop \le k \mathop < n} \floor {\dfrac {m k + x} n}
      | r = \frac {m \paren {n - 1} } 2 + x - S
      | c = from $(1)$
}}
{{eqn | r = \frac {m \paren {n - 1} } 2 + x - d \paren {\dfrac {t \paren {x \bmod d} } n + \frac {t - 1} 2}
      | c = 
}}
{{eqn | r = \frac {m \paren {n - 1} } 2 + x - x \bmod d - \frac {n - d} 2
      | c = 
}}
{{eqn | r = \frac {m \paren {n - 1} } 2 + x - x + d \floor {\frac x d} - \frac {n - 1} 2 + \frac {d - 1} 2
      | c = {{Defof|Modulo Operation}} and algebra
}}
{{eqn | r = \frac {\paren {m - 1} \paren {n - 1} } 2 + \frac {d - 1} 2 + d \floor {\frac x d}
      | c = simplification
}}
{{end-eqn}}
{{qed}}