The question Getting a bound on the coefficients of the factor polynomial got very nice answers on Gelfond's theorem. But for work on proof theory of arithmetic I want a proof in arithmetic. The published proofs use Mahler measure defined in complex analysis. Are there published proofs of Gelfond's theorem in arithmetic in the first place. I should say, proofs published in English or some Western European language. I cannot read Gelfond's paper in Russian.

In fact Mahler uses the sort of complex analysis which is probably conservative over Peano arithmetic along the lines of Takeuti's "A Conservative Extension of Peano Arithmetic." But I am not skilled at that yet. Can anyone here tell me if that will work for Mahler measure? or won't? Or point me to a better source?

Emil Jeřábek asks reasonably if I need Gelfond's theorem. In fact I do need something close to it. I want polynomial factorization over algebraic number fields. This is probably best approached in terms of two-variable integer polynomials where the first variable is really to be taken modulo an irreducible polynomial over $\mathbb{Z}$. This would be a pretty special case of Gelfond's theorem, but not obviously reducible to one-variable polynomials over $\mathbb{Z}$.

To be clear I am asking to know a proof, so I can check if it works in EFA. The project is to establish that EFA suffices for the classical Galois theory of number fields inclduing the Artin-Schreier theorem -- which is not obvious, since results in Reverse Math show even PRA does not suffice for the more general theory of algebraic extensions of $\mathbb{Q}$.