$p$-adic logarithm is a homomorphism, formal power series proof Consider the $p$-adic logarithm defined by the series
$$\log (1+x) = \sum_{n\ge 1} (-1)^{n+1} \frac{x^n}{n}.$$
It converges for $|x|_p < 1$, and if $|x|_p < 1$ and $|y|_p < 1$, then we have
$$\log ((1+x)\cdot (1+y)) = \log (1+x) + \log (1+y).$$
One way to show it is to note that in the ring of formal power series $\mathbb{Q} [[X,Y]]$ (where $\log (1+X)$ is defined by the same formula) we have
$$\log ((1+X)\cdot (1+Y)) = \log (1+X) + \log (1+Y).$$
How does one see that this formal identity indeed implies the identity above?
We have to see that
$$\sum_{n\ge 1} (-1)^{n+1}\,\frac{(x+y+xy)^n}{n} = \sum_{n\ge 1} (-1)^{n+1}\,\left(\frac{x^n}{n} + \frac{y^n}{n}\right).$$
Let us expand the term $(x+y+xy)^n$:
$$(x+y+xy)^n = \sum_{i_1 + i_2 + i_3 = n} {n \choose i_1, i_2, i_3} \, x^{i_1}\,y^{i_2}\,(xy)^{i_3} = \sum_{i_1 + i_2 + i_3 = n} {n \choose i_1, i_2, i_3}\,x^{i_1+i_3}\,y^{i_2+i_3} = \sum_{i\ge 0} \sum_{j\ge 0} {n \choose n-j, n-i, i+j-n}\,x^i\,y^j.$$
We have then
$$\sum_{n\ge 1} (-1)^{n+1}\,\frac{(x+y+xy)^n}{n} = \sum_{n\ge 1} \sum_{i\ge 0} \sum_{j\ge 0} \frac{(-1)^{n+1}}{n}\,{n \choose n-j, n-i, i+j-n}\,x^i\,y^j.$$
Now the order of sums $\sum_{n\ge 1} \sum_{i\ge 0} \sum_{j\ge 0}$ may be changed (I will go back to this point below) to obtain
$$\sum_{i\ge 0} \sum_{j\ge 0} \sum_{n\ge 1} \frac{(-1)^{n+1}}{n}\,{n \choose n-j, n-i, i+j-n}\,x^i\,y^j,$$
and we have to see that the numbers
$$c_{ij} = \sum_{n\ge 1} \frac{(-1)^{n+1}}{n}\,{n \choose n-j, n-i, i+j-n}$$
satisfy
$$c_{ij} = \begin{cases}
(-1)^{m+1}/m, & \text{if }i = m, j = 0 \text{ or } i = 0, j = m,\\
0, & \text{otherwise}.
\end{cases}$$
But we already know that it's true thanks to the formal identity in $\mathbb{Q} [[X,Y]]$, so we are done.

The only non-formal step in the above is changing the order of sums. Recall that in the non-archimedian case, we have
$$\sum_{i\ge 0} \sum_{j\ge 0} x_{ij} = \sum_{j\ge 0} \sum_{i\ge 0} x_{ij}$$
if $|x_{ij}| \to 0$ as $\max (i,j) \to \infty$.
In the above case, we may note that
$$\left|\sum_{j\ge 0} \frac{(-1)^{n+1}}{n}\,{n \choose n-j, n-i, i+j-n}\,x^i\,y^j\right|_p \xrightarrow{\max (n,i) \to \infty} 0$$
(by the way, is it completely obvious?) so that
$$\sum_{n\ge 1} \sum_{i\ge 0} \sum_{j\ge 0} \frac{(-1)^{n+1}}{n}\,{n \choose n-j, n-i, i+j-n}\,x^i\,y^j = \sum_{i\ge 0} \sum_{n\ge 1} \sum_{j\ge 0} \frac{(-1)^{n+1}}{n}\,{n \choose n-j, n-i, i+j-n}\,x^i\,y^j = \sum_{i\ge 0} \sum_{j\ge 0} \sum_{n\ge 1} \frac{(-1)^{n+1}}{n}\,{n \choose n-j, n-i, i+j-n}\,x^i\,y^j$$
(we swap the two inner sums in the second equality since they are finite).

My question is the following: all these details look a bit messy. Is there a shorter justification of the transition from the formal identity to the corresponding identity with $p$-adic series?
Koblitz in his GTM 58 book says that since in the non-archimedian situation, any convergent series converges after an arbitrary reordering, we can automatically assume that we may write
$$\sum_{n\ge 1} (-1)^{n+1}\,\frac{(x+y+xy)^n}{n} = \sum_{i\ge 0}\sum_{j\ge 0} c_{ij}\,x^i\,y^j,$$
for some $c_{ij}$. Maybe I am missing something obvious, and the above change of summation order indeed doesn't require any explicit justifications?
Thank you.
 A: It’s always possible that I have misunderstood the thrust of your question, but perhaps this argument will satisfy the preconditions you have set:
Set $G(x,y)=\log\bigl[(1+x)(1+y)\bigr]$ and $H(x,y)=\log(1+x)+\log(1+y)$. Take the derivative of each with respect to $x$. From $G$, you get
$$
\frac1{(1+x)(1+y)}\frac\partial{\partial x}\bigl[(1+x)(1+y)\bigr]=\frac1{1+x}\,,
$$
while from $H$ you get, of course, $\frac1{1+x}$. So $G$ and $H$ differ by a $y$-series:
$$
\log\bigl[(1+x)(1+y)\bigr]=K(y)+\log(1+x)+\log(1+y)\,.
$$
Now substitute $x=0$ and get $K=0$.
A: For a shorter proof, the main idea is simple: you evaluate the formal identity at $(X,Y) = (x,y)$ to get the special identity. Everything else is technical detail.
To address a concern in the comments, the point is that evaluation is continuous. If $\sum a_k x^k$ is a convergent power series in a topological ring $R$, then any continuous homomorphism $\varphi : R \to S$ will satisfy
$$ \varphi\left( \sum_{k=0}^{\infty} a_k x^k \right) = \varphi\left( \lim_{n \to \infty} \sum_{k=0}^{n} a_k x^k \right)
= \lim_{n \to \infty} \varphi\left( \sum_{k=0}^{n} a_k x^k \right)
\\= \lim_{n \to \infty} \sum_{k=0}^n \varphi(a_k) \varphi(x)^k 
= \sum_{k=0}^\infty \varphi(a_k) \varphi(x)^k 
$$
In particular, if $\log(1+z)$ is defined in $R$, then $\log(1 + \varphi(z))$ is defined in $S$ and $\varphi(\log(1+z)) = \log(1+\varphi(z))$.

The main technical obstacle is the fact that the power series $\log(1+T)$ does not have $\mathbb{Z}_p$-integral coefficients, so we can't directly invoke many of the usual facts about power series rings. 
So, one must instead develop enough of the theory of convergent formal power series to show the homomorphisms involved are defined and continuous. Unfortunately, I don't recall how straightforward this is; but maybe your source already has the relevant theorems.
