Theorem: Cauchy's Mean Theorem

Let $x_1, x_2, \ldots, x_n \in \R$ be real numbers which are all positive.
Let $A_n$ be the arithmetic mean of $x_1, x_2, \ldots, x_n$.
Let $G_n$ be the geometric mean of $x_1, x_2, \ldots, x_n$.
Then:
:$A_n \ge G_n$
with equality holding {{iff}}:
:$\forall i, j \in \set {1, 2, \ldots, n}: x_i = x_j$
That is, {{iff}} all terms are equal.

Proof:
The arithmetic mean of $x_1, x_2, \ldots, x_n$ is defined as:
:$\ds A_n = \frac 1 n \paren {\sum_{k \mathop = 1}^n x_k}$
The geometric mean of $x_1, x_2, \ldots, x_n$ is defined as:
:$\ds G_n = \paren {\prod_{k \mathop = 1}^n x_k}^{1/n}$
We prove the result by induction:
For all $n \in \Z_{>0}$, let $\map P n$ be the proposition:
:For all positive real numbers $x_1, x_2, \ldots, x_n: A_n \ge G_n$.
$\map P 1$ is true, as this just says:
:$\dfrac {x_1} 1 \ge {x_1}^{1/1}$
which is trivially true.
=== Basis for the Induction ===
$\map P 2$ is the case:
:$\dfrac {x_1 + x_2} 2 \ge \sqrt {x_1 x_2}$
As $x_1, x_2 > 0$ we can take their square roots and do the following:
{{begin-eqn}}
{{eqn | l = 0
      | o = \le
      | r = \paren {\sqrt {x_1} - \sqrt {x_2} }^2
      | c = 
}}
{{eqn | r = x_1 - 2\sqrt {x_1 x_2} + x_2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sqrt {x_1 x_2}
      | o = \le
      | r = \frac {x_1 + x_2} 2
      | c = 
}}
{{end-eqn}}
This is our basis for the induction.
=== Induction Hypothesis ===
Now we show that:
:$(1): \quad$ If $\map P {2^k}$ is true, where $k \ge 1$, then it logically follows that $\map P {2^{k + 1} }$ is true
:$(2): \quad$ If $\map P k$ is true, where $k \ge 2$, then it logically follows that $\map P {k - 1}$ is true.
The result will follow by Forward-Backward Induction.
This is our first induction hypothesis:
:$A_{2^k} \ge G_{2^k}$
Then we need to show:
:$A_{2^{k + 1} } \ge G_{2^{k + 1} }$
=== Induction Step ===
This is our induction step:
Let $m = 2^k$.
Then $2^{k + 1} = 2 m$.
Because $\map P m$ is true:
:$\paren {x_1 x_2 \dotsm x_m}^{1/m} \le \dfrac 1 m \paren {x_1 + x_2 + \dotsb + x_m}$
Also:
:$\paren {x_{m + 1} x_{m + 2} \dotsm x_{2 m} }^{1/m} \le \dfrac 1 m \paren {x_{m + 1} + x_{m + 2} + \dotsb + x_{2 m} }$
But we have $\map P 2$, so:
:$\paren {\paren {x_1 x_2 \dotsm x_m}^{1/m} \paren {x_{m + 1} x_{m + 2} \dotsm x_{2 m} }^{1/m} }^{1/2} \le \dfrac 1 2 \paren {\dfrac {x_1 + x_2 + \cdots + x_m} m + \dfrac {x_{m + 1} + x_{m + 2} + \dotsb + x_{2 m} } m}$
So:
:$\paren {x_1 x_2 \dotsm x_{2 m} }^{1/2m} \le \dfrac {x_1 + x_2 + \dotsb + x_{2 m} } {2 m}$
So $\map P {2 m} = \map P {2^{k + 1} }$ holds.
So $\map P {2^n}$ holds for all $n$ by induction.
Now suppose $\map P k$ holds.
Then:
{{begin-eqn}}
{{eqn | l = \paren {x_1 x_2 \dotsm x_{k - 1} G_{k - 1} }^{1/k}
      | o = \le
      | r = \dfrac {x_1 + x_2 + \dotsm + x_{k - 1} + G_{k - 1} } k
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {G_{k - 1}^{k - 1} G_{k - 1} }^{1/k}
      | o = \le
      | r = \dfrac {\paren {k - 1} A_{k - 1} + G_{k - 1} } k
      | c = 
}}
{{eqn | ll= \leadsto
      | l = k G_{k - 1}
      | o = \le
      | r = \paren {k - 1} A_{k - 1} + G_{k - 1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {k - 1} G_{k - 1}
      | o = \le
      | r = \paren {k - 1} A_{k - 1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = G_{k - 1}
      | o = \le
      | r = A_{k - 1}
      | c = 
}}
{{end-eqn}}
So $\map P k \implies \map P {k - 1}$ and the result follows by Forward-Backward Induction.
Therefore $A_n \ge G_n$ for all $n$.
{{qed}}