It doesn't seem to me that you need any choice principle at all to prove that this series converges. The Alternating Series Test that appears in any elementary calculus books seems to do the job, and doesn't seem to require any amount of AC. If $\Sigma_n (-1)^n a_n$ is an alternating series, with $a_n$ descending to $0$, then the finite partial sums up to positive term are descending and the partial sums up to a negative term are increasing, and that these two sequences converge to the same limit.

So I'm not sure which theorem had been "called upon to show" that the series converges, but unless I am mistaken, it must have been something other than what our students would call the Alternating Series Test.

Edit. More generally, I claim that the convergence of a series can never depend on the Axiom of Choice. Suppose that $r=\langle a_0,a_1,\ldots\rangle$ is a sequence of real numbers, and we are consider the series $\Sigma a_n$. The assertion "$\Sigma a_n$ converges" is a statement about $r$ having complexity $\Sigma^1_1$, that is, an analytic fact about $r$, and therefore has the same truth value in the set theoretic universe $V$ as it has in the relativized constructible universe $L[r]$, where AC holds. In particular, the series converges in $V$ if and only if it converges in $L[r]$.

Conclusion. If you have a series $\Sigma a_n$ defined in a sufficiently concrete manner and you can prove in ZFC that it converges, then you can prove in ZF that it converges.

(The technical requirement here about sufficiently concrete is that the description of $r=\langle a_0,a_1,\ldots\rangle$ should be absolute from $V$ to $L[r]$. This would be true of any arithmetically definable series as in the question, defined by an arithmetic formula, or even a Borel definition or a $\Sigma^1_2$ definition.)

It doesn't seem to me that you need any choice principle at all to prove that this series converges. The Alternating Series Test that appears in any elementary calculus books seems to do the job, and doesn't seem to require any amount of AC. If $\Sigma_n (-1)^n a_n$ is an alternating series, with $a_n$ descending to $0$, then the finite partial sums up to positive term are descending and the partial sums up to a negative term are increasing, and that these two sequences converge to the same limit.

So I'm not sure which theorem had been "called upon to show" that the series converges, but unless I am mistaken, it must have been something other than what our students would call the Alternating Series Test.

Edit. More generally, I claim that the convergence of a series can never depend on the Axiom of Choice. Suppose that $r=\langle a_0,a_1,\ldots\rangle$ is a sequence of real numbers, and we are consider the series $\Sigma a_n$. The assertion "$\Sigma a_n$ converges" is a statement about $r$ having complexity $\Sigma^1_1(r)$, that is, an analytic fact about $r$, and therefore has the same truth value in the set theoretic universe $V$ as it has in the relativized constructible universe $L[r]$, where AC holds. In particular, the series converges in $V$ if and only if it converges in $L[r]$.

Conclusion. If you have a series $\Sigma a_n$ defined in a sufficiently concrete manner and you can prove in ZFC that it converges, then you can prove in ZF that it converges.

(The technical requirement here about sufficiently concrete is that the description of $r=\langle a_0,a_1,\ldots\rangle$ should be absolute from $V$ to $L[r]$. This would be true of any arithmetically definable series as in the question, defined by an arithmetic formula, or even a Borel definition or a $\Sigma^1_2$ definition.)

It doesn't seem to me that you need any choice principle at all to prove that this series converges. The Alternating Series Test that appears in any elementary calculus books seems to do the job, and doesn't seem to require any amount of AC. If $\Sigma_n (-1)^n a_n$ is an alternating series, with $a_n$ descending to $0$, then the finite partial sums up to positive term are descending and the partial sums up to a negative term are increasing, and that these two sequences converge to the same limit.

So I'm not sure which theorem had been "called upon to show" that the series converges, but unless I am mistaken, it must have been something other than what our students would call the Alternating Series Test.

It doesn't seem to me that you need any choice principle at all to prove that this series converges. The Alternating Series Test that appears in any elementary calculus books seems to do the job, and doesn't seem to require any amount of AC. If $\Sigma_n (-1)^n a_n$ is an alternating series, with $a_n$ descending to $0$, then the finite partial sums up to positive term are descending and the partial sums up to a negative term are increasing, and that these two sequences converge to the same limit.

So I'm not sure which theorem had been "called upon to show" that the series converges, but unless I am mistaken, it must have been something other than what our students would call the Alternating Series Test.

Edit. More generally, I claim that the convergence of a series can never depend on the Axiom of Choice. Suppose that $r=\langle a_0,a_1,\ldots\rangle$ is a sequence of real numbers, and we are consider the series $\Sigma a_n$. The assertion "$\Sigma a_n$ converges" is a statement about $r$ having complexity $\Sigma^1_1$, that is, an analytic fact about $r$, and therefore has the same truth value in the set theoretic universe $V$ as it has in the relativized constructible universe $L[r]$, where AC holds. In particular, the series converges in $V$ if and only if it converges in $L[r]$.

Conclusion. If you have a series $\Sigma a_n$ defined in a sufficiently concrete manner and you can prove in ZFC that it converges, then you can prove in ZF that it converges.

(The technical requirement here about sufficiently concrete is that the description of $r=\langle a_0,a_1,\ldots\rangle$ should be absolute from $V$ to $L[r]$. This would be true of any arithmetically definable series as in the question, defined by an arithmetic formula, or even a Borel definition or a $\Sigma^1_2$ definition.)