Partial zeta values as finite Fourier sums of Bernoulli values

Let $N$ be a natural number with $N \neq 0$, let $k$ be a natural number with $2 \le k$, and let $a \in \mathbb{Z}/N\mathbb{Z}$. The assertion is an identity in $\mathbb{C}$ between the unconditional sum $\sum'$ over the subtype $\{d : \mathbb{Z} \mid (d \bmod N) = a\}$ of the quantities $((d : \mathbb{C})^k)^{-1}$ — that is, the sum of $d^{-k}$ over all integers $d$ congruent to $a$ modulo $N$, the term $d = 0$ (present only when $a = 0$) contributing $(0^k)^{-1} = 0$ because $k \ge 2$ — and the finite expression

where $\psi =$ ZMod.stdAddChar is the standard additive character of $\mathbb{Z}/N\mathbb{Z}$, $x \mapsto e^{2\pi i \tilde x/N}$, regarded in $\mathbb{C}$, $\tilde r =$ r.val $\in \{0,\dots,N-1\}$ is the least non-negative representative of $r$, $B_k$ is the $k$-th Bernoulli polynomial (bernoulliFun k, evaluated at a real argument and then coerced to $\mathbb{C}$), and $k!$ and $N$ are read in $\mathbb{C}$. Note that the sign in the prefactor is that of $-(2\pi i)^k$.

This is the classical evaluation of the partial zeta value $\sum_{d \equiv a\ (N)} d^{-k}$ for $k \ge 2$ as a finite Fourier transform, over $\mathbb{Z}/N\mathbb{Z}$, of the Bernoulli values $B_k(\tilde r/N)$; in particular the left-hand side lies in $(2\pi i)^k \cdot \mathbb{Q}(e^{2\pi i/N})$. It is used in the computation of the constant terms of Eisenstein series, being cited by EisensteinSeries.tsum_inv_cube_congr_one_ne_zero_and_exists_isIntegral.