A (discrete) group is amenable if it admits a finitely additive probability measure (on all its subsets), invariant under left translation. It is a basic fact that every abelian group is amenable. But the proof I know is surprisingly convoluted. I'd like to know if there's a more direct proof.
The proof I know runs as follows.
Every finite group is amenable (in a unique way). This is trivial.
$\mathbb{Z}$ is amenable. This is not trivial as far as I know; the proof I know involves choosing a non-principal ultrafilter on $\mathbb{N}$. This means that $\mathbb{Z}$ is amenable in many different ways, i.e. there are many measures on it, but apparently you can't write down any measure 'explicitly' (without using the Axiom of Choice).
The direct product of two amenable groups is amenable. This isn't exactly trivial, but the measure on the product is at least constructed canonically from the two given measures.
Every finitely generated abelian group is amenable. This follows from 1--3 and the classification theorem.
The class of amenable groups is closed under direct limits (=colimits over a directed poset). This is like step 2: it seems that there's no canonical way of constructing a measure on the direct limit, given measures on each of the groups that you start with; and the proof involves choosing a non-principal ultrafilter on the poset.
Every abelian group is amenable. This follows from 4 and 5, since every abelian group is the direct limit of its finitely generated subgroups.
Is there a more direct proof? Is there even a one-step proof?
Update Yemon Choi suggests an immediate simplification: replace 1 and 4 by
1'. Every quotient of an amenable group is amenable. This is simple: just push the measure forward.
4'. Every f.g. abelian group is amenable, by 1', 2 and 3.
This avoids using the classification theorem for f.g. abelian groups.
Tom Church mentions the possibility of skipping steps 1--3 and going straight to 4. If I understand correctly, this doesn't use the classification theorem either. The argument is similar to the one for $\mathbb{Z}$: one still has to choose an ultrafilter on $\mathbb{N}$. (One also constructs a Følner sequence on the group, a part of the argument which I didn't mention previously but was there all along).
Yemon, Tom and Mariano Suárez-Alvarez all suggest using one or other alternative formulations of amenability. I'm definitely interested in answers like that, but it also reminds me of the old joke:
Tourist: Excuse me, how do I get to Edinburgh Castle from here?
Local: I wouldn't start from here if I were you.
In other words, if a proof of the amenability of abelian groups uses a different definition of amenability than the one I gave, then I want to take the proof of equivalence into account when assessing the simplicity of the overall proof.
Jim Borger points out that if, as seems to be the case, even the proof that $\mathbb{Z}$ is amenable makes essential use of the Axiom of Choice, then life is bound to be hard. I take his point. However, one simplification to the 6-step proof that I'd like to see is a merging of steps 2 and 5. These are the two really substantial steps, but they're intriguingly similar. None of the answers so far seem to make this economy. That is, every proof suggested seems to involve two separate Følner-type arguments.