BTW, the *very* slick proof goes:
- an integer is a rational number s.t. $\norm{x}_p \leq 1$ for all $p$
- use $p$-adic norm on the equation an algebraic integer satisfies:
  $\norm{x^n}_p + \dots + \norm{a_0}_p$
  =
  $\norm{x}^n_p + \dots + \norm{a_0}_p$
    ...and the rest has norm at most $\norm{x}^{n-1}_p$
    so $\norm{x}_p \leq 1$.
  (this is "clearing denominators" in a very abstract way)

What's the point?
It shows that we don't need the particular form of rationals
or unique factorization: we just need to measure divisibility
(via a *norm*).

...and then showing that there are no integer solutions is easy.
