I have seen in a lecture the following identity for the Chebysheff $\psi$ function: $$\psi(x) = x-\log(2\pi)\; - \sum_{\zeta(\rho)=0}\frac{x^\rho}{\rho} \\ = x-\log(2\pi)\; - \frac{1}{2}\log(1-\frac{1}{x^2}) \\ -\sum_{k=1}^{\infty}\frac{2}{|\rho_k|}x^{\Re(\rho_k)}\cos[\Im(\rho_k)\log(x)-\arg(\rho_k)] $$
The first identity is famous and I can find derivations of that, also the log expression for the trivial zeros ($\frac{1}{2}\log(1-\frac{1}{x^2})$) is clear to me. I cannot understand where the one for the non-trivial zeros $\rho_k$ comes from. The expression is mentioned also in the context of the "music of primes" for more or less obvious reasons. Can someone explain if this expression is correct and how to derive it?
Group two conjugate nontrivial zeros, say $\rho_k = \sigma_k + i t_k$ with $t_k > 0$ and write $\rho_k = \lvert\rho_k\rvert e^{i \alpha_k}$. Then
\begin{align} \frac{x^{\rho_k}}{\rho_k} + \frac{x^{\overline{\rho_k}}}{\overline{\rho_k}} &= \frac{x^{\sigma_k}}{\lvert \rho_k\rvert}\bigl(x^{it_k}e^{-i\alpha_k} + x^{-it_k}e^{i\alpha_k}\bigr) \\ &= \frac{x^{\sigma_k}}{\lvert \rho_k\rvert}\cdot 2\Re \bigl(x^{it_k}e^{-i\alpha_k}\bigr) \tag{$z + \overline{z} = 2\Re z$}\\ &= 2\frac{x^{\sigma_k}}{\lvert \rho_k\rvert}\cdot \Re e^{it_k\log x - i\alpha_k} \tag{$x^w = e^{w\log x}$}\\ &= 2\frac{x^{\sigma_k}}{\lvert \rho_k\rvert}\cdot \cos \bigl(t_k\log x - \alpha_k\bigr) \tag{$\Re e^{iy} = \cos y$}\\ &= \frac{2}{\lvert\rho_k\rvert} x^{\Re \rho_k}\cos \bigl(\Im \rho_k(\log x) - \operatorname{arg} \rho_k\bigr). \end{align}