[proofplan]
We first isolate the analytic input: the truncated Perron kernel equals the indicator of $y>1$ up to an explicit oscillatory error. Then we substitute the absolutely convergent Dirichlet series into the vertical integral and justify the exchange of summation and integration by absolute convergence on the line $\operatorname{Re}(s)=c$. Applying the kernel estimate with $y=x/n$ gives the stated error term, and the condition $x \notin \mathbb{N}$ ensures that $y=1$ never occurs.
[/proofplan]
[step:Estimate the truncated Perron kernel away from the transition point]
Fix $c>0$ and $T \geq 1$. Let $\mathcal{L}^1$ denote one-dimensional Lebesgue measure on $\mathbb{R}$. Define the truncated Perron kernel $K_T:(0,\infty)\setminus\{1\}\to\mathbb{C}$ by
\begin{align*}
K_T(y)
:=
\frac{1}{2\pi i}\int_{c-iT}^{c+iT}\frac{y^s}{s}\,ds.
\end{align*}
We prove that there is an absolute constant $C_0>0$ such that, for every $y>0$ with $y\neq 1$,
\begin{align*}
\left|K_T(y)-\mathbb{1}_{(1,\infty)}(y)\right|
\leq
C_0 y^c \min\left\{1,\frac{1}{T|\log y|}\right\}.
\end{align*}
Put $u:=\log y$, so $u\neq 0$. Parametrising the vertical line by the map $\gamma:[-T,T]\to\mathbb{C}$, $t\mapsto c+it$, gives
\begin{align*}
K_T(y)
=
\frac{y^c}{2\pi}\int_{-T}^{\,T}\frac{e^{itu}}{c+it}\,d\mathcal{L}^1(t).
\end{align*}
Taking real parts symmetrically yields
\begin{align*}
K_T(y)
=
\frac{y^c}{\pi}\int_0^{\,T} \frac{c\cos(tu)+t\sin(tu)}{c^2+t^2}\,d\mathcal{L}^1(t).
\end{align*}
If $T|u|\leq 1$, then $|\sin(tu)|\leq t|u|$ for $0\leq t\leq T$, and therefore
\begin{align*}
|K_T(y)|
&\leq
\frac{y^c}{\pi}\int_0^{\,T} \frac{c}{c^2+t^2}\,d\mathcal{L}^1(t)
+
\frac{y^c}{\pi}\int_0^{\,T} \frac{t^2|u|}{c^2+t^2}\,d\mathcal{L}^1(t) \\
&\leq
\frac{y^c}{2}+\frac{y^c}{\pi}T|u|
\leq
\left(\frac{1}{2}+\frac{1}{\pi}\right)y^c.
\end{align*}
For $0<y<1$ this already gives
\begin{align*}
\left|K_T(y)-\mathbb{1}_{(1,\infty)}(y)\right|
\leq
\left(\frac{1}{2}+\frac{1}{\pi}\right)y^c.
\end{align*}
For $y>1$, the same estimate and $y^c\geq 1$ give
\begin{align*}
\left|K_T(y)-1\right|
\leq
1+|K_T(y)|
\leq
\left(\frac{3}{2}+\frac{1}{\pi}\right)y^c.
\end{align*}
Thus the desired uniform estimate holds in the case $T|u|\leq 1$ with the absolute constant $C_1:=3/2+1/\pi$.
It remains to prove the sharper estimate when $T|u|>1$. Suppose first that $y>1$, so $u>0$. For $R>0$, let $Q_R$ be the positively oriented rectangle with vertical sides $\operatorname{Re}(s)=c$ and $\operatorname{Re}(s)=-R$ and horizontal sides $\operatorname{Im}(s)=\pm T$. The meromorphic map $s\mapsto y^s/s$ has exactly one pole in $Q_R$, namely a simple pole at $s=0$ with residue $1$. By the residue theorem applied to this rectangle,
\begin{align*}
K_T(y)-1
=
-\frac{1}{2\pi i}\int_{-R+iT}^{c+iT}\frac{y^s}{s}\,ds
-\frac{1}{2\pi i}\int_{-R-iT}^{-R+iT}\frac{y^s}{s}\,ds
-\frac{1}{2\pi i}\int_{c-iT}^{-R-iT}\frac{y^s}{s}\,ds.
\end{align*}
On either horizontal side, with $s=\sigma\pm iT$ and $-R\leq \sigma\leq c$, we have $|s|\geq T$ and $|y^s|=e^{\sigma u}$, hence
\begin{align*}
\left|\int_{-R}^{c}\frac{y^{\sigma\pm iT}}{\sigma\pm iT}\,d\mathcal{L}^1(\sigma)\right|
\leq
\frac{1}{T}\int_{-R}^{c}e^{\sigma u}\,d\mathcal{L}^1(\sigma)
\leq
\frac{y^c}{T u}.
\end{align*}
On the left side, if $R>T$, then $|-R+it|\geq R-T$ for $-T\leq t\leq T$, so
\begin{align*}
\left|\int_{-T}^{\,T}\frac{y^{-R+it}}{-R+it}\,d\mathcal{L}^1(t)\right|
\leq
\frac{2T e^{-Ru}}{R-T}\to 0
\end{align*}
as $R\to\infty$. Letting $R\to\infty$ gives
\begin{align*}
|K_T(y)-1|
\leq
\frac{1}{\pi}\frac{y^c}{T\log y}.
\end{align*}
Now suppose that $0<y<1$, so $u<0$. For $R>c$, close the rectangle to the right with vertical sides $\operatorname{Re}(s)=c$ and $\operatorname{Re}(s)=R$. This rectangle contains no pole of $s\mapsto y^s/s$. The same residue computation gives $K_T(y)$ as the negative of the two horizontal integrals and the right vertical integral. On either horizontal side,
\begin{align*}
\left|\int_c^R \frac{y^{\sigma\pm iT}}{\sigma\pm iT}\,d\mathcal{L}^1(\sigma)\right|
\leq
\frac{1}{T}\int_c^R e^{\sigma u}\,d\mathcal{L}^1(\sigma)
\leq
\frac{y^c}{T|u|}.
\end{align*}
The right vertical side is bounded by
\begin{align*}
\left|\int_{-T}^{\,T}\frac{y^{R+it}}{R+it}\,d\mathcal{L}^1(t)\right|
\leq
\frac{2T e^{Ru}}{R-T}\to 0
\end{align*}
as $R\to\infty$ through values $R>T$. Therefore
\begin{align*}
|K_T(y)|
\leq
\frac{1}{\pi}\frac{y^c}{T|\log y|}.
\end{align*}
Combining the cases $T|\log y|\leq 1$ and $T|\log y|>1$ proves the claimed estimate with
\begin{align*}
C_0:=\max\left\{\frac{3}{2}+\frac{1}{\pi},\frac{1}{\pi}\right\}.
\end{align*}
[guided]
The goal is to compare the finite vertical integral with the discontinuous cutoff $\mathbb{1}_{(1,\infty)}(y)$. Let $\mathcal{L}^1$ denote one-dimensional Lebesgue measure on $\mathbb{R}$, and put $u:=\log y$. Since $y\neq 1$, we have $u\neq 0$. After parametrising the vertical segment by $s=c+it$, the kernel becomes
\begin{align*}
K_T(y)
=
\frac{y^c}{2\pi}\int_{-T}^{\,T}\frac{e^{itu}}{c+it}\,d\mathcal{L}^1(t).
\end{align*}
Pairing the terms at $t$ and $-t$ gives the real integral
\begin{align*}
K_T(y)
=
\frac{y^c}{\pi}\int_0^{\,T} \frac{c\cos(tu)+t\sin(tu)}{c^2+t^2}\,d\mathcal{L}^1(t).
\end{align*}
This representation controls the transition region $T|u|\leq 1$. In that region $|\sin(tu)|\leq t|u|$ for $0\leq t\leq T$, so
\begin{align*}
|K_T(y)|
&\leq
\frac{y^c}{\pi}\int_0^{\,T} \frac{c}{c^2+t^2}\,d\mathcal{L}^1(t)
+
\frac{y^c}{\pi}\int_0^{\,T} \frac{t^2|u|}{c^2+t^2}\,d\mathcal{L}^1(t) \\
&\leq
\frac{y^c}{2}+\frac{y^c}{\pi}T|u|
\leq
\left(\frac{1}{2}+\frac{1}{\pi}\right)y^c.
\end{align*}
If $0<y<1$, the cutoff is $0$, so this bounds $|K_T(y)-\mathbb{1}_{(1,\infty)}(y)|$. If $y>1$, then $y^c\geq 1$, and the triangle inequality gives
\begin{align*}
|K_T(y)-1|
\leq
1+|K_T(y)|
\leq
\left(\frac{3}{2}+\frac{1}{\pi}\right)y^c.
\end{align*}
This proves the uniform part of the estimate with an explicit absolute constant.
Away from the transition region, we use a finite rectangular contour and then pass to a limit with explicit side estimates. Suppose $y>1$, so $u>0$. For $R>0$, let $Q_R$ be the positively oriented rectangle with vertical sides $\operatorname{Re}(s)=c$ and $\operatorname{Re}(s)=-R$ and horizontal sides $\operatorname{Im}(s)=\pm T$. The map $s\mapsto y^s/s$ is meromorphic and has exactly one pole in this rectangle, a simple pole at $s=0$ with residue $1$. The residue theorem gives
\begin{align*}
K_T(y)-1
=
-\frac{1}{2\pi i}\int_{-R+iT}^{c+iT}\frac{y^s}{s}\,ds
-\frac{1}{2\pi i}\int_{-R-iT}^{-R+iT}\frac{y^s}{s}\,ds
-\frac{1}{2\pi i}\int_{c-iT}^{-R-iT}\frac{y^s}{s}\,ds.
\end{align*}
On the horizontal sides, write $s=\sigma\pm iT$. Then $|s|\geq T$ and $|y^s|=e^{\sigma u}$, so
\begin{align*}
\left|\int_{-R}^{c}\frac{y^{\sigma\pm iT}}{\sigma\pm iT}\,d\mathcal{L}^1(\sigma)\right|
\leq
\frac{1}{T}\int_{-R}^{c}e^{\sigma u}\,d\mathcal{L}^1(\sigma)
\leq
\frac{y^c}{T u}.
\end{align*}
On the left vertical side, if $R>T$, then $|-R+it|\geq R-T$, hence
\begin{align*}
\left|\int_{-T}^{\,T}\frac{y^{-R+it}}{-R+it}\,d\mathcal{L}^1(t)\right|
\leq
\frac{2T e^{-Ru}}{R-T}\to 0
\end{align*}
as $R\to\infty$. Therefore
\begin{align*}
|K_T(y)-1|
\leq
\frac{1}{\pi}\frac{y^c}{T\log y}.
\end{align*}
For $0<y<1$, we close the rectangle to the right instead, because $y^s=e^{s\log y}$ decays as $\operatorname{Re}(s)\to+\infty$. The right-hand rectangle contains no pole. The two horizontal sides satisfy
\begin{align*}
\left|\int_c^R \frac{y^{\sigma\pm iT}}{\sigma\pm iT}\,d\mathcal{L}^1(\sigma)\right|
\leq
\frac{1}{T}\int_c^R e^{\sigma u}\,d\mathcal{L}^1(\sigma)
\leq
\frac{y^c}{T|u|},
\end{align*}
and the right vertical side satisfies
\begin{align*}
\left|\int_{-T}^{\,T}\frac{y^{R+it}}{R+it}\,d\mathcal{L}^1(t)\right|
\leq
\frac{2T e^{Ru}}{R-T}\to 0
\end{align*}
as $R\to\infty$ through values $R>T$. Hence
\begin{align*}
|K_T(y)|
\leq
\frac{1}{\pi}\frac{y^c}{T|\log y|}.
\end{align*}
The transition estimate handles $T|\log y|\leq 1$, while the contour estimate handles $T|\log y|>1$. Thus the full bound follows with
\begin{align*}
C_0:=\max\left\{\frac{3}{2}+\frac{1}{\pi},\frac{1}{\pi}\right\}.
\end{align*}
[/guided]
[/step]
[step:Interchange the Dirichlet series with the truncated vertical integral]
For $s=c+it$ with $t\in[-T,T]$, absolute convergence at real part $c>\sigma_a$ gives
\begin{align*}
\sum_{n=1}^{\infty}|a_n n^{-s}|
=
\sum_{n=1}^{\infty}|a_n|n^{-c}
<\infty.
\end{align*}
Moreover,
\begin{align*}
\int_{-T}^{\,T}
\sum_{n=1}^{\infty}
\left|
a_n n^{-c-it}\frac{x^{c+it}}{c+it}
\right|
\,d\mathcal{L}^1(t)
\leq
x^c
\left(\int_{-T}^{\,T}\frac{1}{|c+it|}\,d\mathcal{L}^1(t)\right)
\sum_{n=1}^{\infty}|a_n|n^{-c}
<\infty.
\end{align*}
Let $\#_{\mathbb{N}}$ denote counting measure on $\mathbb{N}$. Thus the hypotheses of Tonelli's theorem and [Fubini's theorem](/theorems/2961) for the product measure $\mathcal{L}^1\otimes\#_{\mathbb{N}}$ are satisfied: the displayed non-negative majorant has finite integral over $[-T,T]\times\mathbb{N}$. Hence absolute convergence justifies termwise integration on the finite segment. Parametrising $s=c+it$ gives
\begin{align*}
\frac{1}{2\pi i}\int_{c-iT}^{c+iT}F(s)\frac{x^s}{s}\,ds
&=
\sum_{n=1}^{\infty}
a_n
\frac{1}{2\pi i}\int_{c-iT}^{c+iT}
\frac{(x/n)^s}{s}\,ds \\
&=
\sum_{n=1}^{\infty} a_n K_T(x/n).
\end{align*}
[/step]
[step:Compare the kernel sum with the sharp cutoff sum]
Since $x\notin\mathbb{N}$, we have $x/n\neq 1$ for every $n\in\mathbb{N}$. Also,
\begin{align*}
\mathbb{1}_{(1,\infty)}(x/n)
=
\mathbb{1}_{\{n<x\}}.
\end{align*}
Because $x$ is not an integer, the conditions $n<x$ and $n\leq x$ are equivalent for $n\in\mathbb{N}$. Hence
\begin{align*}
\sum_{n\leq x}a_n
=
\sum_{n=1}^{\infty}a_n\mathbb{1}_{(1,\infty)}(x/n).
\end{align*}
Using the identity from the previous step and subtracting, we obtain
\begin{align*}
\sum_{n\leq x}a_n
-
\frac{1}{2\pi i}\int_{c-iT}^{c+iT}F(s)\frac{x^s}{s}\,ds
=
\sum_{n=1}^{\infty}
a_n\left(\mathbb{1}_{(1,\infty)}(x/n)-K_T(x/n)\right).
\end{align*}
Taking absolute values and applying the kernel estimate with $y=x/n$ gives
\begin{align*}
\left|
\sum_{n\leq x}a_n
-
\frac{1}{2\pi i}\int_{c-iT}^{c+iT}F(s)\frac{x^s}{s}\,ds
\right|
&\leq
C_0
\sum_{n=1}^{\infty}
|a_n|
\left(\frac{x}{n}\right)^c
\min\left\{1,\frac{1}{T|\log(x/n)|}\right\}.
\end{align*}
The constant $C_0$ is absolute, so this is exactly the asserted $O$-term. This proves the truncated Perron formula.
[/step]