schoen: Well done! Your proof is much neater than mine.
Now I believe we're well on the way to proving the full challenge. That is to prove:
HM <= GM <= AM <= RMS
Harmonic mean is N / (1/x1 + 1/x2 + ... + 1/xN). RMS is of course the root mean squared, not that other RMS. Equality holds if and only if all numbers in the multiset are equal.
There might be some other means which fit into the chain of inequalities. If anyone knows of them, please let us know.
Does anyone else think there would be much call for some kind of web log devoted to hobby/recreational mathematics?