December 1st
Today I learned the formalization of the intuition that $\ZZ_p$ consists of "formal power series evaluated at $p.$'' This is made explicit in the isomorphism\[\frac{\ZZ[[x]]}{(x-p)}\cong\ZZ_p.\]Namely, modding out a function field by $(x-\alpha)$ is typically the equivalent of evaluating at $\alpha,$ so the above isomorphism is the rigorous way of "plugging in $p$'' into a generating function.
Proving this is not terribly exciting, though it is somewhat satisfying. We do this with the homomorphism theorem, unsurprisingly. Namely, define $\varphi:\ZZ[[x]]\to\ZZ_p$ by\[\sum_{k=0}^\infty c_kx^k\stackrel\varphi\longmapsto(a_n)_{n=0}^\infty,\,a_n=\sum_{k=0}^nc_kp^k,\]where $(a_n)$ is supposed to be a Cauchy sequence in $\ZZ_p.$ This makes the plugging in by $p$ rigorous. Indeed, it is Cauchy because, for $n \gt m$ (without loss of generality),\[|a_n-a_m|_p=\left|\sum_{k=m+1}^nc_kp^k\right|\le\max_{m+1\le k\le n}\left|c_kp^k\right|_p\le\frac1{p^{m+1}},\]which goes to $0$ as $m,n\to\infty.$ Also, $\varphi$ is a homomorphism by the way addition and multiplication are defined in each ring. In particular,\begin{align*} \varphi\left(\sum_{k=0}^\infty c_kx^k\right)+\varphi\left(\sum_{k=0}^\infty d_kx^k\right)&=\left(\sum_{k=0}^nc_kp^k\right)_{n=0}^\infty+\left(\sum_{k=0}^nd_kp^k\right)_{n=0}^\infty \\ &=\left(\sum_{k=0}^n(c_k+d_k)p^k\right)_{n=0}^\infty \\ &=\varphi\left(\sum_{k=0}^\infty(c_k+d_k)x^k\right),\end{align*}and similar for multiplication. This isn't terribly interesting.
To show the desired isomorphism, the interesting parts are showing that $\varphi$ is surjective and with kernel $(x-p),$ which will finish by the homomorphism theorem. Showing surjectivity is easier. For some $a\in\ZZ_p,$ we can associate it with the Cauchy sequence $a=(a_1,a_2,\ldots)$ where $a_\bullet\equiv a\pmod{p^\bullet}$ and $a_\bullet\in[0,p^\bullet).$ Alternatively, this follows directly from the $\varprojlim\ZZ/p^\bullet\ZZ$ definition. Now define $a_0=0$ and let\[P(x)=\sum_{k=0}^\infty\left(\frac{a_{k+1}-a_k}{p^k}\right)x^k.\]This is in $\ZZ[[x]]$ because $p^k\mid a_{k+1}-a_k$ by definition of $a.$ We claim $\varphi(P)=a.$ Indeed,\[\varphi(P)=\left(\sum_{k=0}^n\left(\frac{a_{k+1}-a_k}{p^k}\right)p^k\right)_{n=0}^\infty=\left(\sum_{k=0}^n(a_{k+1}-a_k)\right)_{n=0}^\infty=(a_{n+1})_{n=0}^\infty.\]This sequence is exactly $(a_1,a_2,\ldots)=a,$ so we've successfully found an input $P\in\ZZ[[x]]$ for each $a\in\ZZ_p.$
The main trickery comes with evaluating the kernel. We want to show $(x-p)=\ker(\varphi).$ Quickly, observe that $\varphi(p-x)=(p,0,0,0,\ldots),$ which converges to $0\in\ZZ_p.$ This tells us $x-p\in\ker(\varphi),$ so $(x-p)\subseteq\ker(\varphi)$ as well because $\ker(\varphi)$ is an ideal. It remains to show the reverse inclusion. Pick up any $P\in\ker(\varphi),$ named $P(x)=\sum c_kx^k.$ We would like to construct a polynomial $Q(x)\in\ZZ[[x]]$ such that\[P(x)=(x-p)Q(x).\]However, $x-p$ is a unit in $\QQ[[x]],$ so we can go ahead and compute $Q(x)$ as if this were an equation in $\QQ[[x]].$ Indeed, it should be\[Q(x)=\frac{P(x)}{x-p}=-\frac1p\cdot\frac1{1-(x/p)}\cdot P(x)=-\frac1p\left(\sum_{\ell=0}^\infty\frac{x^\ell}{p^\ell}\right)\left(\sum_{k=0}^\infty c_kx^k\right)\]using infinite geometric series. This multiplies out to\[Q(x)=\sum_{n=0}^\infty\left(-\frac1p\sum_{k=0}^n\frac{c_k}{p^{n-k}}\right)x^n=\sum_{n=0}^\infty\left(-\frac1{p^{n+1}}\sum_{k=0}^nc_kp^k\right)x^n.\]We use $P\in\ker(\varphi)$ in order to show $Q(x)\in\ZZ[[x]].$ In particular, we know that as $n\to\infty,$ we have\[a_n=\sum_{k=0}^nc_kp^k\to0.\]It follows that for all sufficiently large $N,$ we have $|a_N|_p \lt 1/p^{n+1},$ so $p^{n+1}\mid a_N.$ Choosing any $N$ bigger than $n,$ we see that\[\sum_{k=0}^nc_kp^k\equiv a_N\equiv0\pmod{p^{n+1}}.\]It follows that the coefficients of $Q(x)$ are indeed integers. Because $\ZZ[[x]]$ is embedded in $\QQ[[x]],$ the fact that all polynomials in\[P(x)=\sum_{k=0}^\infty c_kx^k=(x-p)\left(\sum_{n=0}^\infty\left(\frac1{p^{n+1}}\sum_{k=0}^nc_kp^k\right)x^n\right)=(x-p)Q(x)\]are in $\ZZ[[x]]$ means that we can read this equation as in $\ZZ[[x]].$ It follows that $P(x)\in(x-p),$ so we are done here.
This completes the proof. As an aside, this proof can be pretty much lifted directly into a proof that $\ZZ((x))/(x-p)\cong\QQ_p,$ where $\ZZ((x))$ is $\QQ((x))$ with integer coefficients. Notably, $\ZZ((x))$ is not closed under inversion. The only complication is that we have to allow for negative terms, but the finite negative terms of $\ZZ((x))$ match up directly with the finite negative terms of $\QQ_p,$ so it works out.