avewright/proofwiki-math huggingface dataset:
Theorem: Square Matrix is Row Equivalent to Triangular Matrix

Let $\mathbf A = \sqbrk a_n$ be a square matrix of order $n$ over a commutative ring $R$.
Then $\mathbf A$ can be converted to an upper or lower triangular matrix by elementary row operations.

Proof:
This proof assumes that $R$ is a field, which makes the triangulation process slightly quicker.
By this assumptions, all elements of $\mathbf A$ have multiplicative inverses.
Let $\mathbf A$ be a square matrix of order $n$.
We proceed by induction on $n$, the number of rows of $\mathbf A$.
=== Basis for the Induction ===
For $n = 1$, we have a matrix of just one element, which is trivially diagonal, hence both upper and lower triangular.
This is the basis for the induction.
=== Induction Hypothesis ===
Fix $n \in \N$, and assume all $n \times n$-matrices can be upper triangularised by elementary row operations. 
If $R$ is a field, assume all $n \times n$-matrices can be upper triangularised by elementary row operations of type $2$.
This forms our induction hypothesis.
=== Induction Step ===
Let $\mathbf A = \sqbrk a_{n + 1}$ be a square matrix of order $n + 1$.
When the first column of $\mathbf A$ contains only zeroes, it is upper triangularisable {{iff}} the submatrix $\map {\mathbf A} {1; 1}$ is.
Each elementary row operation used in triangularisation process of the submatrix $\map {\mathbf A} {1; 1}$ will not change the zeros of the first column of $\mathbf A$.
So when $\map {\mathbf A} {1; 1}$ is upper triangularised, then $\mathbf A$ will also be upper triangularised.
From the induction hypothesis, we conclude that $\mathbf A$ can be upper triangularised by elementary row operations.
Now suppose that its first column contains a non-zero value.
Suppose that $a_{1 1} = 0$.
Let $j$ be the smallest row index such that $a_{j 1} \ne 0$, and note that $j$ exists by assumption.
Now apply the following operation of type $2$:
:$r_1 \to r_1 + r_j$
As $a_{j 1} \ne 0$, this enforces $a_{1 1} \ne 0$, and we continue as in the case below.
Suppose $a_{1 1} \ne 0$. 
We use the following operations of type $2$:
:$\forall j \in \set {2, \ldots, n + 1}: r_j \to r_j - \dfrac {a_{j 1}} {a_{1 1}} r_1$
This will put the first column to zero (except for the first element, $a_{1 1}$).
It follows that $\mathbf A$ can be upper triangularised {{iff}} the submatrix $\map {\mathbf A} {1; 1}$ can.
Again, the induction hypothesis renders $\mathbf A$ upper triangularisable by elementary row operations.
This completes the case distinction, and hence the result follows by induction.
To put the matrix $\mathbf A$ into lower triangular form, just do the same thing, but start with the last column and the last diagonal element $a_{n + 1 \; n + 1}$.
{{qed}}
Theorem: Product of Triangular Matrices

Let $\mathbf A = \sqbrk a_n, \mathbf B = \sqbrk b_n$ be upper triangular matrices of order $n$.
Let $\mathbf C = \mathbf A \mathbf B$.
Then
:$(1): \quad$ the diagonal elements of $\mathbf C$ are given by:
::::$\forall j \in \closedint 1 n: c_{j j} = a_{j j} b_{j j}$
:::That is, the diagonal elements of $\mathbf C$ are those of the factor matrices multiplied together.
:$(2): \quad$ The matrix $\mathbf C$ is itself upper triangular.
The same applies if both $\mathbf A$ and $\mathbf B$ are lower triangular matrices.

Proof:
From the definition of matrix product, we have:
:$\ds \forall i, j \in \closedint 1 n: c_{i j} = \sum_{k \mathop = 1}^n a_{i k} b_{k j}$
Now when $i = j$ (as on the main diagonal):
:$\ds c_{j j} = \sum_{k \mathop = 1}^n a_{j k} b_{k j}$
Now both $\mathbf A$ and $\mathbf B$ are upper triangular.
Thus:
:if $k > j$, then $b_{k j} = 0$ and thus $a_{j k} b_{k j} = 0$
:if $k < j$, then $a_{j k} = 0$ and thus $a_{j k} b_{k j} = 0$.
So $a_{j k} b_{k j} \ne 0$ only when $j = k$.
So:
:$\ds c_{j j} = \sum_{k \mathop = 1}^n a_{j k} b_{k j} = a_{j j} b_{j j}$
Now if $i > j$, it follows that either $a_{i k}$ or $b_{k j}$ is zero for all $k$, and thus $c_{i j} = 0$.
Thus $\mathbf C$ is upper triangular.
The same argument can be used for when $\mathbf A$ and $\mathbf B$ are both lower triangular matrices.
{{Qed}}
Category:Triangular Matrices
Category:Conventional Matrix Multiplication
8dcua45lkyarfwk6bgoj12lym5ol775
Theorem: Effect of Elementary Row Operations on Determinant

Let $\mathbf A = \sqbrk a_n$ be a square matrix of order $n$.
Let $\map \det {\mathbf A}$ denote the determinant of $\mathbf A$.
Let $i, j \in \closedint 1 n : i \neq j$ be indices of the rows of $\mathbf A$.
Take the elementary row operations:
{{begin-axiom}}
{{axiom | n = \text {ERO} 1
        | t = For some $\lambda$, multiply row $i$ by $\lambda$
        | m = r_i \to \lambda r_i
}}
{{axiom | n = \text {ERO} 2
        | t = For some $\lambda$, add $\lambda$ times row $j$ to row $i$
        | m = r_i \to r_i + \lambda r_j
}}
{{axiom | n = \text {ERO} 3
        | t = Exchange rows $i$ and $j$
        | m = r_i \leftrightarrow r_j
}}
{{end-axiom}}
Applying $\text {ERO} 1$ has the effect of multiplying $\map \det {\mathbf A}$ by $\lambda$.
Applying $\text {ERO} 2$ has no effect on $\map \det {\mathbf A}$.
Applying $\text {ERO} 3$ has the effect of multiplying $\map \det {\mathbf A}$ by $-1$.

Proof:
From Elementary Row Operations as Matrix Multiplications, an elementary row operation on $\mathbf A$ is equivalent to matrix multiplication by the elementary row matrices corresponding to the elementary row operations.
From Determinant of Elementary Row Matrix, the determinants of those elementary row matrices are as follows:
Theorem: Modulus in Terms of Conjugate

Let $z = a + i b$ be a complex number.
Let $\cmod z$ be the modulus of $z$.
Let $\overline z$ be the conjugate of $z$.
Then:
:$\cmod z = \sqrt {z \overline z}$

Proof:
Let $z = a + i b$.
Then:
{{begin-eqn}}
{{eqn | l = z \overline z
      | r = a^2 + b^2
      | c = Product of Complex Number with Conjugate
}}
{{eqn | r = \cmod z^2
      | c = {{Defof|Complex Modulus}}
}}
{{eqn | ll= \leadsto
      | l = \cmod z
      | r = \sqrt {z \overline z}
      | c = taking square root of both sides
}}
{{end-eqn}}
{{qed}}
Theorem: Existence and Uniqueness of Positive Root of Positive Real Number

Let $x \in \R$ be a real number such that $x \ge 0$.
Let $n \in \Z$ be an integer such that $n \ne 0$.
Then there always exists a unique $y \in \R: \paren {y \ge 0} \land \paren {y^n = x}$.
Hence the justification for the terminology '''the positive $n$th root of $x$''' and the notation $x^{1/n}$.
=== Positive Exponent ===
{{:Existence and Uniqueness of Positive Root of Positive Real Number/Positive Exponent}}
=== Negative Exponent ===
{{:Existence and Uniqueness of Positive Root of Positive Real Number/Negative Exponent}}

Proof:
The result follows from Existence of Positive Root of Positive Real Number and Uniqueness of Positive Root of Positive Real Number.
{{qed}}
Theorem: Even Power is Non-Negative

Let $x \in \R$ be a real number.
Let $n \in \Z$ be an even integer.
Then $x^n \ge 0$.
That is, all even powers are positive.

Proof:
Let $n \in \Z$ be an even integer.
Then $n = 2 k$ for some $k \in \Z$.
Thus:
:$\forall x \in \R: x^n = x^{2 k} = \paren {x^k}^2$
But from Square of Real Number is Non-Negative:
:$\forall x \in \R: \paren {x^k}^2 \ge 0$
and so there is no real number whose square is negative.
The result follows from Solution to Quadratic Equation.
{{Qed}}
Theorem: Sign of Odd Power

Let $x \in \R$ be a real number.
Let $n \in \Z$ be an odd integer.
Then:
:$x^n = 0 \iff x = 0$
:$x^n > 0 \iff x > 0$
:$x^n < 0 \iff x < 0$
That is, the sign of an odd power matches the number it is a power of.

Proof:
If $n$ is an odd integer, then $n = 2 k + 1$ for some $k \in \N$.
Thus $x^n = x \cdot x^{2 k}$.
But $x^{2 k} \ge 0$ from Even Power is Non-Negative.
The result follows.
{{qed}}
Theorem: Product of Absolute Values on Ordered Integral Domain

Let $\struct {D, +, \times, \le}$ be an ordered integral domain whose zero is denoted by $0_D$.
For all $a \in D$, let $\size a$ denote the absolute value of $a$.
Then:
:$\size a \times \size b = \size {a \times b}$

Proof:
Let $P$ be the (strict) positivity property on $D$.
Let $<$ be the (strict) total ordering defined on $D$ as:
:$a < b \iff a \le b \land a \ne b$
Let $N$ be the strict negativity property on $D$.
We consider all possibilities in turn.
$(1): \quad a = 0_D$ or $b = 0_D$
In this case, both the {{LHS}} $\size a \times \size b$ and the {{RHS}} are equal to zero.
So:
:$\size a \times \size b = \size {a \times b}$
$(2): \quad \map P a, \map P b$
First:
{{begin-eqn}}
{{eqn | l = \map P a, \map P b
      | o = \leadsto
      | r = \size a = a, \size b = b
      | c = {{Defof|Absolute Value on Ordered Integral Domain}}
}}
{{eqn | o = \leadsto
      | r = \size a \times \size b = a \times b
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \map P a, \map P b
      | o = \leadsto
      | r = \map P {a \times b}
      | c = Strict Positivity Property: $(\text P 2)$
}}
{{eqn | o = \leadsto
      | r = \size {a \times b} = a \times b
      | c = {{Defof|Absolute Value on Ordered Integral Domain}}
}}
{{end-eqn}}
So:
:$\size a \times \size b = \size {a \times b}$
$(3): \quad \map P a, \map N b$
First:
{{begin-eqn}}
{{eqn | l = \map P a, \map N b
      | o = \leadsto
      | r = \size a = a, \size b = -b
      | c = {{Defof|Absolute Value on Ordered Integral Domain}}
}}
{{eqn | o = \leadsto
      | r = \size a \times \size b = -a \times b
      | c = Product with Ring Negative
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \map P a, \map N b
      | o = \leadsto
      | r = \map N {a \times b}
      | c = Properties of Strict Negativity: $(5)$
}}
{{eqn | o = \leadsto
      | r = \map P {-a \times b}
      | c = {{Defof|Strict Negativity Property}}
}}
{{eqn | o = \leadsto
      | r = \size {a \times b} = -a \times b
      | c = {{Defof|Absolute Value on Ordered Integral Domain}}
}}
{{end-eqn}}
So:
:$\size a \times \size b = \size {a \times b}$
Similarly $\map N a, \map P b$.
$(4): \quad \map N a, \map N b$
First:
{{begin-eqn}}
{{eqn | l = \map N a, \map N b
      | o = \leadsto
      | r = \size a = -a, \size b = -b
      | c = {{Defof|Absolute Value on Ordered Integral Domain}}
}}
{{eqn | o = \leadsto
      | r = \size a \times \size b = a \times b
      | c = Product of Ring Negatives
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \map N a, \map N b
      | o = \leadsto
      | r = \map P {a \times b}
      | c = Properties of Strict Negativity: $(4)$
}}
{{eqn | o = \leadsto
      | r = \map P {a \times b}
      | c = {{Defof|Strict Negativity Property}}
}}
{{eqn | o = \leadsto
      | r = \size {a \times b} = a \times b
      | c = {{Defof|Absolute Value on Ordered Integral Domain}}
}}
{{end-eqn}}
So:
:$\size a \times \size b = \size {a \times b}$
In all cases the result holds.
{{qed}}
Theorem: Negative of Absolute Value

Let $x \in \R$ be a real number.
Let $\size x$ denote the absolute value of $x$.
Then:
:$-\size x \le x \le \size x$

Proof:
Either $x \ge 0$ or $x < 0$.
:If $x \ge 0$, then:
::$-\size x \le 0 \le x = \size x$
:If $x < 0$, then:
::$-\size x = x < 0 < \size x$
{{qed}}
Theorem: Order of Squares in Ordered Ring

Let $\struct {R, +, \circ, \le}$ be an ordered ring whose zero is $0_R$ and whose unity is $1_R$.
Let $x, y \in \struct {R, +, \circ, \le}$ such that $0_R \le x, y$.
Then:
:$x \le y \implies x \circ x \le y \circ y$
When $R$ is one of the standard sets of numbers, that is $\Z, \Q, \R$, then this translates into:
:If $x, y$ are positive then $x \le y \implies x^2 \le y^2$.

Proof:
Assume $x \le y$.
As $\le$ is compatible with the ring structure of $\struct {R, +, \circ, \le}$, we have:
:$x \ge 0 \implies x \circ x \le x \circ y$
:$y \ge 0 \implies x \circ y \le y \circ y$
and thus as $\le$ is transitive, it follows that $x \circ x \le y \circ y$.
{{qed}}
Theorem: Least Upper Bound Property

Let $S \subset \R$ be a non-empty subset of the set of real numbers such that $S$ is bounded above.
Then $S$ admits a supremum in $\R$.
This is known as the '''least upper bound property''' of the real numbers.

Proof:
Let $S$ be bounded above.
Let $L$ be the set of real numbers defined as:
:$\alpha \in L \iff \exists x \in S: \alpha < x$
Let $R := \relcomp \R L$, where $\complement_\R$ denotes complement in $\R$.
By construction of $L$, every element of $L$ is less than some element of $S$.
Hence no element of $L$ is an upper bound of $S$.
By construction of $R$, for every element $x$ of $R$, there exists no element of $S$ which is greater than $x$.
Hence every element of $R$ is an upper bound of $S$.
So, to prove the existence of $\sup S$, it is sufficient to demonstrate that $R$ contains a smallest number.
We verify that $L$ and $R$ fulfil the conditions for Dedekind's Theorem to hold.
We confirm that $\tuple {L, R}$ is a Dedekind cut of $\R$:
:$(1): \quad \set {L, R}$ is a partition of $\R$
:$(2): \quad L$ does not have a greatest element
:$(3): \quad \forall x \in L: \forall y \in R: x < y$
By Union with Relative Complement:
:$L \cup R = \R$
By Set with Relative Complement forms Partition, $\tuple {L, R}$ forms a partition of $\R$.
So $(1)$ holds immediately.
Let $\alpha \in L$.
Then there exists $x \in S$ such that $\alpha < x$.
Let $\alpha'$ be such that $\alpha < \alpha' < x$.
Then $\alpha' \in L$
So whatever $\alpha \in L$ is, it cannot be the greatest element of $L$.
Thus $(2)$ holds.
Let $\alpha \in L$.
Let $\beta \in R$.
Then there exists $x \in S$ such that $\alpha < x$.
By construction of $R$, $x \le \beta$.
Thus $\alpha < \beta$ for all $\alpha \in L, \beta \in R$.
Thus $(3)$ holds.
By the corollary to Dedekind's Theorem, either $L$ contains a greatest element or $R$ contains a smallest element.
We have shown that $L$ does not contain a greatest element.
Hence $R$ contains a smallest element.
Hence if $S$ is bounded above, it has a supremum.
Thus $\R$ is Dedekind complete by definition.
Now let $S$ be bounded below.
By Dedekind Completeness is Self-Dual, it follows that $S$ admits an infimum.
{{qed}}
Theorem: Complex Multiplication is Closed

The set of complex numbers $\C$ is closed under multiplication:
:$\forall z, w \in \C: z \times w \in \C$

Proof:
From the informal definition of complex numbers, we define the following:
:$z = x_1 + i y_1$
:$w = x_2 + i y_2$
where $i = \sqrt {-1}$ and $x_1, x_2, y_1, y_2 \in \R$.
Then from the definition of complex multiplication:
:$z w = \paren {x_1 x_2 - y_1 y_2} + i \paren {x_1 y_2 + x_2 y_1}$
From Real Numbers form Field:
:$x_1 x_2 - y_1 y_2 \in \R$
and:
:$x_1 y_2 + x_2 y_1 \in \R$
Hence the result.
{{qed}}
Theorem: Complex Multiplication is Closed

The set of complex numbers $\C$ is closed under multiplication:
:$\forall z, w \in \C: z \times w \in \C$

Proof:
From the formal definition of complex numbers, we define the following:
:$z = \tuple {x_1, y_1}$
:$w = \tuple {x_2, y_2}$
Then from the definition of complex multiplication:
:$z w = \tuple {x_1 x_2 - y_1 y_2, x_1 y_2 + x_2 y_1}$
From Real Numbers form Field:
:$x_1 x_2 - y_1 y_2 \in \R$
and:
:$x_1 y_2 + x_2 y_1 \in \R$
Hence the result.
{{qed}}
Theorem: Complex Multiplication is Associative

The operation of multiplication on the set of complex numbers $\C$ is associative:
:$\forall z_1, z_2, z_3 \in \C: z_1 \paren {z_2 z_3} = \paren {z_1 z_2} z_3$

Proof:
From the definition of complex numbers, we define the following:
{{begin-eqn}}
{{eqn | l = z_1
      | o = :=
      | r = \tuple {x_1, y_1}
}}
{{eqn | l = z_2
      | o = :=
      | r = \tuple {x_2, y_2}
}}
{{eqn | l = z_3
      | o = :=
      | r = \tuple {x_3, y_3}
}}
{{end-eqn}}
where $x_1, x_2, x_3, y_1, y_2, y_3 \in \R$.
Thus:
{{begin-eqn}}
{{eqn | r = z_1 \left({z_2 z_3}\right)
      | o = 
}}
{{eqn | r = \tuple {x_1, y_1} \paren {\tuple {x_2, y_2} \tuple {x_3, y_3} }
      | c = {{Defof|Complex Number|index = 2}}
}}
{{eqn | r = \tuple {x_1, y_1} \tuple {x_2 x_3 - y_2 y_3, x_2 y_3 + y_2 x_3}
      | c = {{Defof|Complex Number/Definition 2/Multiplication|Complex Multiplication}}
}}
{{eqn | r = \tuple {x_1 \paren {x_2 x_3 - y_2 y_3} - y_1 \paren {x_2 y_3 + y_2 x_3}, y_1 \paren {x_2 x_3 - y_2 y_3} + x_1 \paren {x_2 y_3 + y_2 x_3} }
      | c = {{Defof|Complex Number/Definition 2/Multiplication|Complex Multiplication}}
}}
{{eqn | r = \tuple {x_1 x_2 x_3 - x_1 y_2 y_3 - y_1 x_2 y_3 - y_1 y_2 x_3, y_1 x_2 x_3 - y_1 y_2 y_3 + x_1 x_2 y_3 + x_1 y_2 x_3}
      | c = Real Multiplication Distributes over Addition
}}
{{eqn | r = \tuple {\paren {x_1 x_2 x_3 - y_1 y_2 x_3} - \paren {x_1 y_2 y_3 + y_1 x_2 y_3}, \paren {x_1 x_2 y_3 - y_1 y_2 y_3} + \paren {y_1 x_2 x_3 + x_1 y_2 x_3} }
      | c = Real Multiplication is Commutative
}}
{{eqn | r = \tuple {\paren {x_1 x_2 - y_1 y_2} x_3 - \paren {x_1 y_2 + y_1 x_2} y_3, \paren {x_1 x_2 - y_1 y_2} y_3 + \paren {x_1 y_2 + y_1 x_2} x_3}
      | c = Real Multiplication Distributes over Addition
}}
{{eqn | r = \tuple {x_1 x_2 - y_1 y_2, x_1 y_2 + y_1 x_2} \tuple {x_3, y_3}
      | c = {{Defof|Complex Number/Definition 2/Multiplication|Complex Multiplication}}
}}
{{eqn | r = \paren {\tuple {x_1, y_1} \tuple {x_2, y_2} } \tuple {x_3, y_3}
      | c = {{Defof|Complex Number/Definition 2/Multiplication|Complex Multiplication}}
}}
{{eqn | r = \paren {z_1 z_2} z_3
      | c = {{Defof|Complex Number|index = 2}}
}}
{{end-eqn}}
{{qed}}
Theorem: Multiple of Supremum

Let $S \subseteq \R: S \ne \O$ be a non-empty subset of the set of real numbers $\R$.
Let $S$ be bounded above.
Let $z \in \R: z > 0$ be a positive real number.
Then:
:$\ds \map {\sup_{x \mathop \in S} } {z x} = z \map {\sup_{x \mathop \in S} } x$

Proof:
Let $B = \map \sup S$.
Then by definition, $B$ is the smallest number such that $x \in S \implies x \le B$.
Let $T = \set {z x: x \in S}$.
Because $z > 0$, it follows that:
:$\forall x \in S: z x \le z B$
So $T$ is bounded above by $z B$.
By the Continuum Property, $T$ has a supremum which we will call $C$.
We need to show that $C = z B$.
Since $z B$ is ''an'' upper bound for $T$, and $C$ is the ''smallest'' upper bound for $T$, it follows that $C \le z B$.
Now as $z > 0$ and is a real number:
:$\exists z^{-1} \in \R: z^{-1} > 0$
So we can reverse the roles of $S$ and $T$:
:$S = \set {z^{-1} y: y \in T}$
We know that $C$ is the smallest number such that:
:$\forall y \in T: y \le C$
So it follows that:
:$\forall y \in T: z^{-1} y \le z^{-1} C$
So $z^{-1} C$ is ''an'' upper bound for $S$.
But $B$ is the ''smallest'' upper bound for $S$.
So:
:$B \le z^{-1} C \implies z B \le C$
So we have shown that:
:$z B \le C$ and $C \le z B$
Hence the result.
{{qed}}
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:
Let:
:$\map f x = \ln x$
for $x > 0$.
With a view to apply Jensen's Inequality: Real Analysis: Corollary, we can show that $f$ is concave on $\openint 0 \infty$. 
By Second Derivative of Concave Real Function is Non-Positive, it is sufficient to show that $\map {f' '} x \le 0$ for all $x > 0$. 
We have, by Derivative of Natural Logarithm:
:$\map {f'} x = \dfrac 1 x$
We then have, by Derivative of Power:
:$\map {f' '} x = -\dfrac 1 {x^2}$ 
As $x^2 > 0$ for all $x > 0$, we have:
:$\dfrac 1 {x^2} > 0$
Therefore: 
:$-\dfrac 1 {x^2} = \map {f' '} x < 0$
so $f$ is indeed concave on $\openint 0 \infty$.
As $x_1, x_2, \ldots, x_n$ are all positive, they all lie in the interval $\openint 0 \infty$. 
We therefore have, by Jensen's Inequality: Real Analysis: Corollary: 
:$\ds \map \ln {\frac {\sum_{k \mathop = 1}^n \lambda_k x_k} {\sum_{k \mathop = 1}^n \lambda_k} } \ge \frac {\sum_{k \mathop = 1}^n \lambda_k \map \ln {x_k} } {\sum_{k \mathop = 1}^n \lambda_k}$
for real $\lambda_1, \lambda_2, \ldots, \lambda_n \ge 0$, with at least one of which being non-zero. 
As $n$ is a positive integer, we have: 
:$\dfrac 1 n > 0$
We can therefore set: 
:$\lambda_i = \dfrac 1 n$
for $1 \le i \le n$.
This gives: 
{{begin-eqn}}
{{eqn | l = \map \ln {\frac {\sum_{k \mathop = 1}^n \lambda_k x_k} {\sum_{k \mathop = 1}^n \lambda_k} }
      | r = \map \ln {\frac {\sum_{k \mathop = 1}^n x_k} {n \sum_{k \mathop = 1}^n \frac 1 n} }
}}
{{eqn | r = \map \ln {\frac {\sum_{k \mathop = 1}^n x_k} n}
}}
{{eqn | r = \map \ln {A_n}
      | c = {{Defof|Arithmetic Mean}}
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \frac {\sum_{k \mathop = 1}^n \lambda_k \map \ln {x_k} } {\sum_{k \mathop = 1}^n \lambda_k}
      | r = \frac {\sum_{k \mathop = 1}^n \map \ln {x_k} } {n \sum_{k \mathop = 1}^n \frac 1 n}
}}
{{eqn | r = \frac {\sum_{k \mathop = 1}^n \map \ln {x_k} } n
}}
{{eqn | r = \frac 1 n \map \ln {\prod_{k \mathop = 1}^n x_k}
      | c = Sum of Logarithms
}}
{{eqn | r = \map \ln {\paren {\prod_{k \mathop = 1}^n x_k}^{1/n} }
      | c = Logarithm of Power
}}
{{eqn | r = \map \ln {G_n}
      | c = {{Defof|Geometric Mean}}
}}
{{end-eqn}}
We therefore have: 
:$\map \ln {A_n} \ge \map \ln {G_n}$
Note that for $x > 0$: 
:$\dfrac 1 x = \map {f'} x > 0$
Therefore, by Derivative of Monotone Function, $f$ is increasing on $\openint 0 \infty$. 
We therefore have: 
:$A_n \ge G_n$
{{qed}}
Theorem: Distance on Real Numbers is Metric

Let $x, y \in \R$ be real numbers.
Let $\map d {x, y}$ be the distance between $x$ and $y$:
:$\map d {x, y} = \size {x - y}$
Then $\map d {x, y}$ is a metric on $\R$.
Thus it follows that $\tuple {\R, d}$ is a metric space.

Proof:
We check the metric space axioms in turn.
Theorem: Convergent Sequence in Metric Space is Bounded

Let $M = \struct {A, d}$ be a metric space.
Let $\sequence {x_n}$ be a sequence in $M$ which is convergent, and so $x_n \to l$ as $n \to \infty$.
Then $\sequence {x_n}$ is bounded.

Proof:
Let $M = \struct {A, d}$ be a metric space.
Let $\sequence {x_n}$ be a sequence in $M$ which is convergent, and so $x_n \to l$ as $n \to \infty$.
From the definition, in order to prove boundedness, all we need to do is find $K \in \R$ such that $\forall n \in \N: \map d {x_n, l} \le K$.
Since $\sequence {x_n}$ converges, it is true that:
:$\forall \epsilon > 0: \exists N: n > N \implies \map d {x_n, l} < \epsilon$
In particular, this is true when $\epsilon = 1$, for example.
That is:
:$\exists N_1: \forall n > N_1: \map d {x_n, l} < 1$
So now we set:
:$K = \max \set {\map d {x_1, l}, \map d {x_2, l}, \ldots, \map d {x_{N_1}, l}, 1}$
The result follows.
{{qed}}
Theorem: Convergent Sequence Minus Limit

Let $X$ be one of the standard number fields $\Q, \R, \C$.
Let $\sequence {x_n}$ be a sequence in $X$ which converges to $l$.
That is:
: $\ds \lim_{n \mathop \to \infty} x_n = l$
Then:
: $\ds \lim_{n \mathop \to \infty} \cmod {x_n - l} = 0$

Proof:
Let $\epsilon > 0$.
We need to show that there exists $N$ such that:
:$\forall n > N: \size {\paren {\size {x_n - l} - 0} } < \epsilon$
But:
:$\size {\paren {\size {x_n - l} - 0} } = \size {x_n - l}$
So what needs to be shown is just:
:$x_n \to l$ as $n \to \infty$
which is the definition of $\ds \lim_{n \mathop \to \infty} x_n = l$.
{{qed}}
Theorem: Convergent Sequence Minus Limit

Let $X$ be one of the standard number fields $\Q, \R, \C$.
Let $\sequence {x_n}$ be a sequence in $X$ which converges to $l$.
That is:
: $\ds \lim_{n \mathop \to \infty} x_n = l$
Then:
: $\ds \lim_{n \mathop \to \infty} \cmod {x_n - l} = 0$

Proof:
We note that all of $\Q, \R, \C$ can be considered as metric spaces.
Then under the usual metric:
: $\map d {x_n, l} = \cmod {x_n - l}$.
The result follows from the definition of metric:
:$\map d {x_n, l} = 0 \iff x_n = l$.
{{qed}}