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:
=== Necessary Condition ===
Let:
:$\forall i, j \in \set {1, 2, \ldots, n}: x_i = x_j = x$
Then:
{{begin-eqn}}
{{eqn | l = A_n
      | r = \dfrac 1 n \sum_{j \mathop = 1}^n x
      | c = 
}}
{{eqn | r = \dfrac 1 n n x
      | c = 
}}
{{eqn | r = x
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = G_n
      | r = \paren {\prod_{j \mathop = 1}^n x}^{\frac 1 n}
      | c = 
}}
{{eqn | r = \paren {x^n}^{\frac 1 n}
      | c = 
}}
{{eqn | r = x
      | c = 
}}
{{end-eqn}}
So:
:$A_n = G_n = x$
{{qed|lemma}}
=== Sufficient Condition ===
Let $A_n = G_n$.
We prove the result by induction:
For all $n \in \Z_{>0}$, let $\map P n$ be the proposition:
:$A_n = G_n \implies \forall i, j \in \set {1, 2, \ldots, n}: x_i = x_j$
$\map P 1$ is true, as this just says:
{{begin-eqn}}
{{eqn | l = A_1
      | r = G_1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac 1 1 \sum_{j \mathop = 1}^1 x_j
      | r = \paren {\prod_{j \mathop = 1}^1 x_j}^{1/1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x_1
      | r = x_1
      | c = 
}}
{{end-eqn}}
which is trivially true.
==== Basis for the Induction ====
$\map P 2$ is the case:
{{begin-eqn}}
{{eqn | l = A_2
      | r = G_2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {x_1 + x_2} 2
      | r = \sqrt {x_1 x_2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {\dfrac {x_1 + x_2} 2}^2
      | r = x_1 x_2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x_1^2 + 2 x_1 x_2 + x_2^2
      | r = 4 x_1 x_2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x_1^2 - 2 x_1 x_2 + x_2^2
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {x_1 - x_2}^2
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x_1
      | r = x_2
      | c = 
}}
{{end-eqn}}
This is our basis for the induction.
==== Induction Hypothesis ====
Now we show that:
:$(1): \quad$ If $\map P k$ is true, where $k \ge 1$, then it logically follows that $\map P {2 k}$ 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_k = G_k \implies \forall i, j \in \set {1, 2, \ldots, k}: x_i = x_j = x$
Also, let:
:$A_k' := \ds \dfrac 1 k \sum_{j \mathop = k + 1}^{2 k} x_j = y$
and:
:$G_k' := \ds \paren {\prod_{j \mathop = k + 1}^{2 k} }^{1 / k} x_j = y$
By the induction hypothesis:
:$A_k' = G_k' \implies \forall i, j \in \set {k + 1, k + 2, \ldots, 2 k}: x_i = x_j = y$
We need to show:
:$A_{2 k} = G_{2 k} \implies \forall i, j \in \set {1, 2, \ldots, 2 k}: x_i = x_j = x$
==== Induction Step ====
This is our induction step:
Suppose:
:$A_{2 k} = G_{2 k}$
Let:
:$A_k' := \ds \dfrac 1 k \sum_{j \mathop = k + 1}^{2 k} x_j = y$
and:
:$G_k' := \ds \paren {\prod_{j \mathop = k + 1}^{2 k} }^{1 / k} x_j = y$
By the induction hypothesis:
:$A_k' = G_k' \implies \forall i, j \in \set {k + 1, k + 2, \ldots, 2 k}: x_i = x_j = y$
Then:
{{begin-eqn}}
{{eqn | l = A_{2 k}
      | r = \dfrac 1 {2 k} \sum_{j \mathop = 1}^{2 k} x_j
      | c = {{Defof|Arithmetic Mean}}
}}
{{eqn | r = \dfrac 1 {2 k} \paren {\sum_{j \mathop = 1}^k x_j + \sum_{j \mathop = k + 1}^{2 k} x_j}
      | c = 
}}
{{eqn | r = \dfrac 1 2 \paren {\dfrac 1 k \sum_{j \mathop = 1}^k x_j + \dfrac 1 k \sum_{j \mathop = k + 1}^{2 k} x_j}
      | c = 
}}
{{eqn | r = \dfrac 1 2 \paren {A_k + A_k'}
      | c = {{Defof|Arithmetic Mean}}
}}
{{eqn | r = \dfrac 1 2 \paren {x + y}
      | c = Definition of $A_k$ and $A_k'$
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = G_{2 k}
      | r = \paren {\prod_{j \mathop = 1}^{2 k} x_j}^{1 / 2 k}
      | c = {{Defof|Geometric Mean}}
}}
{{eqn | r = \paren {\paren {\prod_{j \mathop = 1}^{2 k} x_j}^{1 / k} }^{1 / 2}
      | c = 
}}
{{eqn | r = \paren {\paren {\prod_{j \mathop = 1}^k x_j}^{1 / k} \times \paren {\prod_{j \mathop = k + 1}^{2 k} x_j}^{1 / k} }^{1 / 2}
      | c = 
}}
{{eqn | r = \paren {G_k G_k'}^{1 / 2}
      | c = {{Defof|Geometric Mean}}
}}
{{eqn | r = \paren {x y}^{1 / 2}
      | c = Definition of $G_k$ and $G_k'$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = A_{2 k}
      | r = G_{2 k}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac 1 2 \paren {x + y}
      | r = \paren {x y}^{1 / 2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = y
      | c = Basis for the Induction
}}
{{end-eqn}}
That is:
:$\forall i, j \in \set {1, 2, \ldots, k}: x_i = x_j = x$
:$\forall i, j \in \set {k + 1, k + 2, \ldots, 2 k}: x_i = x_j = x$
Hence:
:$\forall i, j \in \set {1, 2, \ldots, 2 k}: x_i = x_j = x$
Now suppose $\map P k$ holds.
Then:
{{begin-eqn}}
{{eqn | l = G_{k - 1}
      | r = A_{k - 1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {k - 1} G_{k - 1}
      | r = \paren {k - 1} A_{k - 1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = k G_{k - 1}
      | r = \paren {k - 1} A_{k - 1} + G_{k - 1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {G_{k - 1}^{k - 1} G_{k - 1} }^{1/k}
      | r = \dfrac {\paren {k - 1} A_{k - 1} + G_{k - 1} } k
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {x_1 x_2 \dotsm x_{k - 1} G_{k - 1} }^{1 / k}
      | r = \dfrac {x_1 + x_2 + \dotsm + x_{k - 1} + G_{k - 1} } k
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {x_1 x_2 \dotsm x_{k - 1} G_{k - 1} }^{1 / k}
      | r = \dfrac {x_1 + x_2 + \dotsm + x_{k - 1} + G_{k - 1} } k
      | c = 
}}
{{end-eqn}}
But:
:$\paren {x_1 x_2 \dotsm x_{k - 1} G_{k - 1} }^{1 / k}$ is the geometric mean of $\set {x_1, x_2, \ldots, x_{k - 1}, G_{k - 1} }$
:$\dfrac {x_1 + x_2 + \dotsm + x_{k - 1} + G_{k - 1} } k$ is the arithmetic mean of $\set {x_1, x_2, \ldots, x_{k - 1}, G_{k - 1} }$
We have that $\set {x_1, x_2, \ldots, x_{k - 1}, G_{k - 1} }$ has $k$ elements.
Hence by the induction hypothesis:
:$\forall i, j \in \set {1, 2, \ldots, k - 1}: x_i = x_j = G_{k - 1}$
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$.
:$\forall n \in \N: A_n = G_n \implies \forall i, j \in \set {1, 2, \ldots, n}: x_i = x_j$
{{qed}}