avewright/proofwiki-math huggingface dataset:
Theorem: Existence of Inverse Elementary Row Operation/Exchange Rows

Let $\map \MM {m, n}$ be a metric space of order $m \times n$ over a field $K$.
Let $\mathbf A \in \map \MM {m, n}$ be a matrix. 
Let $\map e {\mathbf A}$ be the elementary row operation which transforms $\mathbf A$ to a new matrix $\mathbf A' \in \map \MM {m, n}$.
{{begin-axiom}}
{{axiom | n = \text {ERO} 3
        | t = Exchange rows $k$ and $l$
        | m = r_k \leftrightarrow r_l
}}
{{end-axiom}}
Let $\map {e'} {\mathbf A'}$ be the inverse of $e$.
Then $e'$ is the elementary row operation:
:$e' := r_k \leftrightarrow r_l$
That is:
:$e' = e$

Proof:
Let $\map e {\mathbf A}$ be the elementary row operation:
:$e := r_k \leftrightarrow r_l$
Thus we have:
{{begin-eqn}}
{{eqn | l = r'_k
      | r = r_l
      | c = 
}}
{{eqn | lo= \text {and}
      | l = r'_l
      | r = r_k
      | c = 
}}
{{end-eqn}}
Now let $\map {e'} {\mathbf A'}$ be the elementary row operation which transforms $\mathbf A'$ to $\mathbf A' '$:
:$e' := r'_k \leftrightarrow r'_l$
Applying $e'$ to $\mathbf A'$ we get:
{{begin-eqn}}
{{eqn | l = r' '_k
      | r = r'_l
      | c = 
}}
{{eqn | lo= \text {and}
      | l = r' '_l
      | r = r'_k
      | c = 
}}
{{eqn | ll= \leadsto
      | l = r' '_k
      | r = r_k
      | c = 
}}
{{eqn | lo= \text {and}
      | l = r' '_l
      | r = r_l
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \mathbf A' '
      | r = \mathbf A
      | c = 
}}
{{end-eqn}}
It is noted that for $e'$ to be an elementary row operation, the only possibility is for it to be as defined.
Theorem: Existence of Inverse Elementary Column Operation/Scalar Product of Column

Let $\map \MM {m, n}$ be a metric space of order $m \times n$ over a field $K$.
Let $\mathbf A \in \map \MM {m, n}$ be a matrix. 
Let $\map e {\mathbf A}$ be the elementary column operation which transforms $\mathbf A$ to a new matrix $\mathbf A' \in \map \MM {m, n}$.
{{begin-axiom}}
{{axiom | n = \text {ECO} 1
        | t = For some $\lambda \in K_{\ne 0}$, multiply column $k$ by $\lambda$
        | m = \kappa_k \to \lambda \kappa_k
}}
{{end-axiom}}
Let $\map {e'} {\mathbf A'}$ be the inverse of $e$.
Then $e'$ is the elementary column operation:
:$e' := \kappa_k \to \dfrac 1 \lambda \kappa_k$

Proof:
Let $\map e {\mathbf A}$ be the elementary column operation:
:$e := \kappa_k \to \lambda \kappa_k$
where $\lambda \ne 0$.
Then $\kappa'_k$ is such that:
:$\forall a'_{k i} \in \kappa'_k: a'_{k i} = \lambda a_{k i}$
Now let $\map {e'} {\mathbf A'}$ be the elementary column operation which transforms $\mathbf A'$ to $\mathbf A' '$:
:$e' := \kappa_k \to \dfrac 1 \lambda \kappa_k$
Because it is stipulated in the definition of an elementary column operation that $\lambda \ne 0$, it follows by definition of a field that $\dfrac 1 \lambda$ exists.
Hence $e'$ is defined.
So applying $e'$ to $\mathbf A'$ we get:
{{begin-eqn}}
{{eqn | q = \forall a' '_{i k} \in \kappa' '_k
      | l = a' '_{i k}
      | r = \dfrac 1 \lambda a'_{i k}
      | c = 
}}
{{eqn | r = \dfrac 1 \lambda \paren {\lambda a_{i k} }
      | c = 
}}
{{eqn | r = a_{i k}
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \forall a' '_{i k} \in \kappa' '_k
      | l = a' '_{i k}
      | r = a_{i k}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \kappa' '_k
      | r = \kappa_k
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \mathbf A' '
      | r = \mathbf A
      | c = 
}}
{{end-eqn}}
It is noted that for $e'$ to be an elementary column operation, the only possibility is for it to be as defined.
Theorem: Existence of Inverse Elementary Column Operation/Add Scalar Product of Column to Another

Let $\map \MM {m, n}$ be a metric space of order $m \times n$ over a field $K$.
Let $\mathbf A \in \map \MM {m, n}$ be a matrix. 
Let $\map e {\mathbf A}$ be the elementary column operation which transforms $\mathbf A$ to a new matrix $\mathbf A' \in \map \MM {m, n}$.
{{begin-axiom}}
{{axiom | n = \text {ECO} 2
        | t = For some $\lambda \in K$, add $\lambda$ times column $l$ to column $k$
        | m = \kappa_k \to \kappa_k + \lambda \kappa_l
}}
{{end-axiom}}
Let $\map {e'} {\mathbf A'}$ be the inverse of $e$.
Then $e'$ is the elementary column operation:
:$e' := \kappa_k \to \kappa_k - \lambda \kappa_l$

Proof:
Let $\map e {\mathbf A}$ be the elementary column operation:
:$e := \kappa_k \to \kappa_k + \lambda r_l$
Then $\kappa'_k$ is such that:
:$\forall a'_{i k} \in \kappa'_k: a'_{i k} = a_{i k} + \lambda a_{i l}$
Now let $\map {e'} {\mathbf A'}$ be the elementary column operation which transforms $\mathbf A'$ to $\mathbf A' '$:
:$e' := \kappa'_k \to \kappa'_k - \lambda \kappa'_l$
Applying $e'$ to $\mathbf A'$ we get:
{{begin-eqn}}
{{eqn | q = \forall a' '_{i k} \in \kappa' '_k
      | l = a' '_{i k}
      | r = a'_{i k} - \lambda a'_{i l}
      | c = 
}}
{{eqn | r = \paren {a_{i k} + \lambda a_{i l} } - \lambda a'_{i l}
      | c = 
}}
{{eqn | r = \paren {a_{i k} + \lambda a_{i l} } - \lambda a_{i l}
      | c = as $\lambda a'_{i l} = \lambda a_{i l}$: column $l$ was not changed by $e$
}}
{{eqn | r = a_{i k}
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \forall a' '_{i k} \in \kappa' '_k
      | l = a' '_{i k}
      | r = a_{i k}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \kappa' '_{i k}
      | r = \kappa_{i k}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \mathbf A' '
      | r = \mathbf A
      | c = 
}}
{{end-eqn}}
It is noted that for $e'$ to be an elementary column operation, the only possibility is for it to be as defined.
Theorem: Existence of Inverse Elementary Column Operation/Exchange Columns

Let $\map \MM {m, n}$ be a metric space of order $m \times n$ over a field $K$.
Let $\mathbf A \in \map \MM {m, n}$ be a matrix. 
Let $\map e {\mathbf A}$ be the elementary column operation which transforms $\mathbf A$ to a new matrix $\mathbf A' \in \map \MM {m, n}$.
{{begin-axiom}}
{{axiom | n = \text {ECO} 3
        | t = Interchange columns $k$ and $l$
        | m = \kappa_k \leftrightarrow \kappa_l
}}
{{end-axiom}}
Let $\map {e'} {\mathbf A'}$ be the inverse of $e$.
Then $e'$ is the elementary column operation:
:$e' := \kappa_k \leftrightarrow \kappa_l$
That is:
:$e' = e$

Proof:
Let $\map e {\mathbf A}$ be the elementary column operation:
:$e := \kappa_k \leftrightarrow \kappa_l$
Thus we have:
{{begin-eqn}}
{{eqn | l = \kappa'_k
      | r = \kappa_l
      | c = 
}}
{{eqn | lo= \text {and}
      | l = \kappa'_l
      | r = \kappa_k
      | c = 
}}
{{end-eqn}}
Now let $\map {e'} {\mathbf A'}$ be the elementary column operation which transforms $\mathbf A'$ to $\mathbf A' '$:
:$e' := \kappa'_k \leftrightarrow \kappa'_l$
Applying $e'$ to $\mathbf A'$ we get:
{{begin-eqn}}
{{eqn | l = \kappa' '_k
      | r = \kappa'_l
      | c = 
}}
{{eqn | lo= \text {and}
      | l = \kappa' '_l
      | r = \kappa'_k
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \kappa' '_k
      | r = \kappa_k
      | c = 
}}
{{eqn | lo= \text {and}
      | l = \kappa' '_l
      | r = \kappa_l
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \mathbf A' '
      | r = \mathbf A
      | c = 
}}
{{end-eqn}}
It is noted that for $e'$ to be an elementary column operation, the only possibility is for it to be as defined.
Theorem: Elementary Column Operations as Matrix Multiplications

Let $e$ be an elementary column operation.
Let $\mathbf E$ be the elementary column matrix of order $n$ defined as:
:$\mathbf E = e \paren {\mathbf I}$
where $\mathbf I$ is the unit matrix.
Then for every $m \times n$ matrix $\mathbf A$:
:$e \paren {\mathbf A} = \mathbf A \mathbf E$
where $\mathbf A \mathbf E$ denotes the conventional matrix product.

Proof:
Let $s, t \in \closedint 1 m$ such that $s \ne t$.
Theorem: Square Root of Number Plus Square Root

:$\ds \sqrt {a + \sqrt b} = \sqrt {\dfrac {a + \sqrt {a^2 - b} } 2} + \sqrt {\dfrac {a - \sqrt {a^2 - b} } 2}$

Proof:
We are given that $a^2 - b > 0$.
Then:
:$a > \sqrt b$
and so $\ds \sqrt {a + \sqrt b}$ is defined on the real numbers.
Let $\ds \sqrt {a + \sqrt b} = \sqrt x + \sqrt y$ where $x, y$ are (strictly) positive real numbers.
Squaring both sides gives:
{{begin-eqn}}
{{eqn | l = a + \sqrt b
      | r = \paren {\sqrt x + \sqrt y}^2
      | c = 
}}
{{eqn | r = x + y + 2 \sqrt {x y}
      | c = 
}}
{{end-eqn}}
Set $x + y = a$ and $\sqrt b = 2 \sqrt {x y}$
{{explain|How do you know that the $a$ and $b$ which are $x + y$ and $2 \sqrt {x y}$ are the same $a$ and $b$ that you started with?
$x$ and $y$ are free to choose. They were introduced by hand, and can be set to any value provided that they satisfy the constraint above. This is similar to the proof of Cardano's Formula.
In that case it needs to be explained. As it stands, it looks as though $x$ and $y$ are pulled out of thin air, with no actual indication that having picked them, they bear the relations given to $a$ and $b$ as presented. It's incredibly confusing for beginners, and others whose abilities and understanding are limited, like me.}}
From $\sqrt b = 2 \sqrt {x y}$ we get:
{{begin-eqn}}
{{eqn | l = \sqrt b
      | r = 2 \sqrt {x y}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = b
      | r = 4 x y
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x y
      | r = \frac b 4
      | c = 
}}
{{end-eqn}}
By Viète's Formulas, $x$ and $y$ are solutions to the quadratic equation:
:$z^2 - a z + \dfrac b 4 = 0$
From Solution to Quadratic Equation:
:$z_{1, 2} = \dfrac {a \pm \sqrt {a^2 - b} } 2$
where $a^2 - b > 0$ (which is a given)
{{explain|the notation $z_{1, 2}$}}
{{WLOG}}:
{{begin-eqn}}
{{eqn | l = x = z_1
      | r = \dfrac {a + \sqrt {a^2 - b} } 2
}}
{{eqn | l = y = z_2
      | r = \dfrac {a - \sqrt {a^2 - b} } 2
}}
{{end-eqn}}
Subsituting into $\ds \sqrt {a + \sqrt b} = \sqrt x + \sqrt y$:
{{begin-eqn}}
{{eqn | l = \sqrt {a + \sqrt b}
      | r = \sqrt x + \sqrt y
      | c = 
}}
{{eqn | r = \sqrt {\dfrac {a + \sqrt {a^2 - b} } 2} + \sqrt {\dfrac {a - \sqrt {a^2 - b} } 2}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Square Root of Number Plus Square Root

:$\ds \sqrt {a + \sqrt b} = \sqrt {\dfrac {a + \sqrt {a^2 - b} } 2} + \sqrt {\dfrac {a - \sqrt {a^2 - b} } 2}$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {\sqrt {\dfrac {a + \sqrt {a^2 - b} } 2} + \sqrt {\dfrac {a - \sqrt {a^2 - b} } 2} }^2
      | r = \dfrac {a + \sqrt {a^2 - b} } 2 + \dfrac {a - \sqrt {a^2 - b} } 2 + 2 \sqrt {\dfrac {a + \sqrt {a^2 - b} } 2} \sqrt {\dfrac {a - \sqrt {a^2 - b} } 2}
      | c = multiplying out
}}
{{eqn | r = a + \sqrt {a + \sqrt {a^2 - b} } \sqrt {a - \sqrt {a^2 - b} }
      | c = simplifying
}}
{{eqn | r = a + \sqrt {a^2 - \paren {a^2 - b} }
      | c = Difference of Two Squares
}}
{{eqn | r = a + \sqrt b
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \sqrt {\dfrac {a + \sqrt {a^2 - b} } 2} + \sqrt {\dfrac {a - \sqrt {a^2 - b} } 2}
      | r = \sqrt {a + \sqrt b}
      | c = taking square root of both sides
}}
{{end-eqn}}
{{finish|Report on the matter of the signs and magnitudes of $a$ and $b$ according to the constraints given}}
{{qed}}
Theorem: Square Root of Number Plus Square Root/Proof 1

Let $a$ and $b$ be (strictly) positive real numbers such that $a^2 - b > 0$.
Then:
{{:Square Root of Number Plus Square Root}}

Proof:
We are given that $a^2 - b > 0$.
Then:
:$a > \sqrt b$
and so $\ds \sqrt {a + \sqrt b}$ is defined on the real numbers.
Let $\ds \sqrt {a + \sqrt b} = \sqrt x + \sqrt y$ where $x, y$ are (strictly) positive real numbers.
Squaring both sides gives:
{{begin-eqn}}
{{eqn | l = a + \sqrt b
      | r = \paren {\sqrt x + \sqrt y}^2
      | c = 
}}
{{eqn | r = x + y + 2 \sqrt {x y}
      | c = 
}}
{{end-eqn}}
Set $x + y = a$ and $\sqrt b = 2 \sqrt {x y}$
{{explain|How do you know that the $a$ and $b$ which are $x + y$ and $2 \sqrt {x y}$ are the same $a$ and $b$ that you started with?
$x$ and $y$ are free to choose. They were introduced by hand, and can be set to any value provided that they satisfy the constraint above. This is similar to the proof of Cardano's Formula.
In that case it needs to be explained. As it stands, it looks as though $x$ and $y$ are pulled out of thin air, with no actual indication that having picked them, they bear the relations given to $a$ and $b$ as presented. It's incredibly confusing for beginners, and others whose abilities and understanding are limited, like me.}}
From $\sqrt b = 2 \sqrt {x y}$ we get:
{{begin-eqn}}
{{eqn | l = \sqrt b
      | r = 2 \sqrt {x y}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = b
      | r = 4 x y
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x y
      | r = \frac b 4
      | c = 
}}
{{end-eqn}}
By Viète's Formulas, $x$ and $y$ are solutions to the quadratic equation:
:$z^2 - a z + \dfrac b 4 = 0$
From Solution to Quadratic Equation:
:$z_{1, 2} = \dfrac {a \pm \sqrt {a^2 - b} } 2$
where $a^2 - b > 0$ (which is a given)
{{explain|the notation $z_{1, 2}$}}
{{WLOG}}:
{{begin-eqn}}
{{eqn | l = x = z_1
      | r = \dfrac {a + \sqrt {a^2 - b} } 2
}}
{{eqn | l = y = z_2
      | r = \dfrac {a - \sqrt {a^2 - b} } 2
}}
{{end-eqn}}
Subsituting into $\ds \sqrt {a + \sqrt b} = \sqrt x + \sqrt y$:
{{begin-eqn}}
{{eqn | l = \sqrt {a + \sqrt b}
      | r = \sqrt x + \sqrt y
      | c = 
}}
{{eqn | r = \sqrt {\dfrac {a + \sqrt {a^2 - b} } 2} + \sqrt {\dfrac {a - \sqrt {a^2 - b} } 2}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Square Root of Number Plus Square Root/Proof 2

Let $a$ and $b$ be (strictly) positive real numbers such that $a^2 - b > 0$.
Then:
{{:Square Root of Number Plus Square Root}}

Proof:
{{begin-eqn}}
{{eqn | l = \paren {\sqrt {\dfrac {a + \sqrt {a^2 - b} } 2} + \sqrt {\dfrac {a - \sqrt {a^2 - b} } 2} }^2
      | r = \dfrac {a + \sqrt {a^2 - b} } 2 + \dfrac {a - \sqrt {a^2 - b} } 2 + 2 \sqrt {\dfrac {a + \sqrt {a^2 - b} } 2} \sqrt {\dfrac {a - \sqrt {a^2 - b} } 2}
      | c = multiplying out
}}
{{eqn | r = a + \sqrt {a + \sqrt {a^2 - b} } \sqrt {a - \sqrt {a^2 - b} }
      | c = simplifying
}}
{{eqn | r = a + \sqrt {a^2 - \paren {a^2 - b} }
      | c = Difference of Two Squares
}}
{{eqn | r = a + \sqrt b
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \sqrt {\dfrac {a + \sqrt {a^2 - b} } 2} + \sqrt {\dfrac {a - \sqrt {a^2 - b} } 2}
      | r = \sqrt {a + \sqrt b}
      | c = taking square root of both sides
}}
{{end-eqn}}
{{finish|Report on the matter of the signs and magnitudes of $a$ and $b$ according to the constraints given}}
{{qed}}
Theorem: Square Root of Number Minus Square Root

:$\ds \sqrt {a - \sqrt b} = \sqrt {\dfrac {a + \sqrt {a^2 - b} } 2} - \sqrt {\dfrac {a - \sqrt {a^2 - b} } 2}$

Proof:
We are given that $a^2 - b > 0$.
Then:
:$a > \sqrt b$
and so $\ds \sqrt {a - \sqrt b}$ is defined on the real numbers.
Let $\ds \sqrt {a - \sqrt b} = \sqrt x - \sqrt y$ where $x, y$ are (strictly) positive real numbers.
Observe that:
:$\ds 0 < \sqrt {a - \sqrt b} = \sqrt x - \sqrt y \implies x > y$
Squaring both sides gives:
{{begin-eqn}}
{{eqn | l = a - \sqrt b
      | r = \paren {\sqrt x - \sqrt y}^2
      | c = 
}}
{{eqn | r = x + y - 2 \sqrt {x y}
      | c = 
}}
{{end-eqn}}
Set $x + y = a$ and $\sqrt b = 2 \sqrt {x y}$
From $\sqrt b = 2 \sqrt {x y}$ we get:
{{begin-eqn}}
{{eqn | l = \sqrt b
      | r = 2 \sqrt {x y}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = b
      | r = 4 x y
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x y
      | r = \frac b 4
      | c = 
}}
{{end-eqn}}
By Viète's Formulas, $x$ and $y$ are solutions to the quadratic equation:
:$z^2 - a z + \dfrac b 4 = 0$
From Solution to Quadratic Equation:
:$z_{1, 2} = \dfrac {a \pm \sqrt {a^2 - b} } 2$
where $a^2 - b > 0$ (which is a given)
Because we have that $x > y$:
{{begin-eqn}}
{{eqn | l = x = z_1
      | r = \dfrac {a + \sqrt {a^2 - b} } 2
}}
{{eqn | l = y = z_2
      | r = \dfrac {a - \sqrt {a^2 - b} } 2
}}
{{end-eqn}}
Subsituting into $\ds \sqrt {a - \sqrt b} = \sqrt x - \sqrt y$:
{{begin-eqn}}
{{eqn | l = \sqrt {a - \sqrt b}
      | r = \sqrt x - \sqrt y
      | c = 
}}
{{eqn | r = \sqrt {\dfrac {a + \sqrt {a^2 - b} } 2} - \sqrt {\dfrac {a - \sqrt {a^2 - b} } 2}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Square Root of Number Minus Square Root

:$\ds \sqrt {a - \sqrt b} = \sqrt {\dfrac {a + \sqrt {a^2 - b} } 2} - \sqrt {\dfrac {a - \sqrt {a^2 - b} } 2}$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {\sqrt {\dfrac {a + \sqrt {a^2 - b} } 2} - \sqrt {\dfrac {a - \sqrt {a^2 - b} } 2} }^2
      | r = \dfrac {a + \sqrt {a^2 - b} } 2 + \dfrac {a - \sqrt {a^2 - b} } 2 - 2 \sqrt {\dfrac {a + \sqrt {a^2 - b} } 2} \sqrt {\dfrac {a - \sqrt {a^2 - b} } 2}
      | c = multiplying out
}}
{{eqn | r = a - \sqrt {a + \sqrt {a^2 - b} } \sqrt {a - \sqrt {a^2 - b} }
      | c = simplifying
}}
{{eqn | r = a - \sqrt {a^2 - \paren {a^2 - b} }
      | c = Difference of Two Squares
}}
{{eqn | r = a - \sqrt b
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \sqrt {\dfrac {a + \sqrt {a^2 - b} } 2} - \sqrt {\dfrac {a - \sqrt {a^2 - b} } 2}
      | r = \sqrt {a - \sqrt b}
      | c = taking square root of both sides
}}
{{end-eqn}}
{{finish|Report on the matter of the signs and magnitudes of $a$ and $b$ according to the constraints given}}
{{qed}}
Theorem: Square Root of Number Minus Square Root/Proof 2

Let $a$ and $b$ be (strictly) positive real numbers such that $a^2 - b > 0$.
Then:
{{:Square Root of Number Minus Square Root}}

Proof:
{{begin-eqn}}
{{eqn | l = \paren {\sqrt {\dfrac {a + \sqrt {a^2 - b} } 2} - \sqrt {\dfrac {a - \sqrt {a^2 - b} } 2} }^2
      | r = \dfrac {a + \sqrt {a^2 - b} } 2 + \dfrac {a - \sqrt {a^2 - b} } 2 - 2 \sqrt {\dfrac {a + \sqrt {a^2 - b} } 2} \sqrt {\dfrac {a - \sqrt {a^2 - b} } 2}
      | c = multiplying out
}}
{{eqn | r = a - \sqrt {a + \sqrt {a^2 - b} } \sqrt {a - \sqrt {a^2 - b} }
      | c = simplifying
}}
{{eqn | r = a - \sqrt {a^2 - \paren {a^2 - b} }
      | c = Difference of Two Squares
}}
{{eqn | r = a - \sqrt b
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \sqrt {\dfrac {a + \sqrt {a^2 - b} } 2} - \sqrt {\dfrac {a - \sqrt {a^2 - b} } 2}
      | r = \sqrt {a - \sqrt b}
      | c = taking square root of both sides
}}
{{end-eqn}}
{{finish|Report on the matter of the signs and magnitudes of $a$ and $b$ according to the constraints given}}
{{qed}}
Theorem: Square Root of Number Minus Square Root/Proof 1

Let $a$ and $b$ be (strictly) positive real numbers such that $a^2 - b > 0$.
Then:
{{:Square Root of Number Minus Square Root}}

Proof:
We are given that $a^2 - b > 0$.
Then:
:$a > \sqrt b$
and so $\ds \sqrt {a - \sqrt b}$ is defined on the real numbers.
Let $\ds \sqrt {a - \sqrt b} = \sqrt x - \sqrt y$ where $x, y$ are (strictly) positive real numbers.
Observe that:
:$\ds 0 < \sqrt {a - \sqrt b} = \sqrt x - \sqrt y \implies x > y$
Squaring both sides gives:
{{begin-eqn}}
{{eqn | l = a - \sqrt b
      | r = \paren {\sqrt x - \sqrt y}^2
      | c = 
}}
{{eqn | r = x + y - 2 \sqrt {x y}
      | c = 
}}
{{end-eqn}}
Set $x + y = a$ and $\sqrt b = 2 \sqrt {x y}$
From $\sqrt b = 2 \sqrt {x y}$ we get:
{{begin-eqn}}
{{eqn | l = \sqrt b
      | r = 2 \sqrt {x y}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = b
      | r = 4 x y
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x y
      | r = \frac b 4
      | c = 
}}
{{end-eqn}}
By Viète's Formulas, $x$ and $y$ are solutions to the quadratic equation:
:$z^2 - a z + \dfrac b 4 = 0$
From Solution to Quadratic Equation:
:$z_{1, 2} = \dfrac {a \pm \sqrt {a^2 - b} } 2$
where $a^2 - b > 0$ (which is a given)
Because we have that $x > y$:
{{begin-eqn}}
{{eqn | l = x = z_1
      | r = \dfrac {a + \sqrt {a^2 - b} } 2
}}
{{eqn | l = y = z_2
      | r = \dfrac {a - \sqrt {a^2 - b} } 2
}}
{{end-eqn}}
Subsituting into $\ds \sqrt {a - \sqrt b} = \sqrt x - \sqrt y$:
{{begin-eqn}}
{{eqn | l = \sqrt {a - \sqrt b}
      | r = \sqrt x - \sqrt y
      | c = 
}}
{{eqn | r = \sqrt {\dfrac {a + \sqrt {a^2 - b} } 2} - \sqrt {\dfrac {a - \sqrt {a^2 - b} } 2}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Exchange of Columns as Sequence of Other Elementary Column Operations

Let $\mathbf A$ be an $m \times n$ matrix.
Let $i, j \in \closedint 1 m: i \ne j$
Let $\kappa_k$ denote the $k$th column of $\mathbf A$ for $1 \le k \le n$:
:$\kappa_k = \begin {pmatrix} a_{1 k} \\ a_{2 k} \\ \vdots \\ a_{m k} \end {pmatrix}$
Let $e$ be the elementary column operation acting on $\mathbf A$ as:
{{begin-axiom}}
{{axiom | n = \text {ERO} 3
        | t = Interchange columns $i$ and $j$
        | m = \kappa_i \leftrightarrow \kappa_j
}}
{{end-axiom}}
Then $e$ can be expressed as a finite sequence of exactly $4$ instances of the other two elementary column operations.
{{begin-axiom}}
{{axiom | n = \text {ERO} 1
        | t = For some $\lambda \in K_{\ne 0}$, multiply column $i$ by $\lambda$
        | m = \kappa_i \to \lambda \kappa_i
}}
{{axiom | n = \text {ERO} 2
        | t = For some $\lambda \in K$, add $\lambda$ times column $j$ to column $i$
        | m = \kappa_i \to \kappa_i + \lambda \kappa_j
}}
{{end-axiom}}

Proof:
In the below:
:$\kappa_i$ denotes the initial state of column $i$
:$\kappa_j$ denotes the initial state of column $j$
:$\kappa_i'$ denotes the state of column $i$ after having had the latest elementary column operation applied
:$\kappa_j'$ denotes the state of column $j$ after having had the latest elementary column operation applied.
$(1)$: Apply $\text {ECO} 2$ to column $j$ for $\lambda = 1$:
:$\kappa_j \to \kappa_j + \kappa_i$
After this operation:
{{begin-eqn}}
{{eqn | l = \kappa_i'
      | r = \kappa_i
}}
{{eqn | l = \kappa_j'
      | r = \kappa_i + \kappa_j
}}
{{end-eqn}}
{{qed|lemma}}
$(2)$: Apply $\text {ECO} 2$ to column $i$ for $\lambda = -1$:
:$\kappa_i \to \kappa_i + \paren {-\kappa_j}$
After this operation:
{{begin-eqn}}
{{eqn | l = \kappa_i'
      | r = \kappa_i - \paren {\kappa_i + \kappa_j}
}}
{{eqn | r = -\kappa_j
}}
{{eqn | l = \kappa_j'
      | r = \kappa_i + \kappa_j
}}
{{end-eqn}}
{{qed|lemma}}
$(3)$: Apply $\text {ECO} 2$ to column $j$ for $\lambda = 1$:
:$\kappa_j \to \kappa_j + \kappa_i$
After this operation:
{{begin-eqn}}
{{eqn | l = \kappa_i'
      | r = -\kappa_j
}}
{{eqn | l = \kappa_j'
      | r = \kappa_i + \kappa_j - \kappa_j
}}
{{eqn | r = \kappa_i
}}
{{end-eqn}}
{{qed|lemma}}
$(4)$: Apply $\text {ECO} 1$ to column $i$ for $\lambda = -1$:
:$\kappa_i \to -\kappa_i$
After this operation:
{{begin-eqn}}
{{eqn | l = \kappa_i'
      | r = -\paren {-\kappa_j}
}}
{{eqn | r = \kappa_j
}}
{{eqn | l = \kappa_j'
      | r = \kappa_i
}}
{{end-eqn}}
{{qed|lemma}}
Thus, after all the $4$ elementary column operations have been applied, we have:
{{begin-eqn}}
{{eqn | l = \kappa_i'
      | r = \kappa_j
}}
{{eqn | l = \kappa_j'
      | r = \kappa_i
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Effect of Elementary Column 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$.
Take the elementary column operations:
{{begin-axiom}}
{{axiom | n = \text {ECO} 1
        | t = For some $\lambda$, multiply column $i$ by $\lambda$
        | m = \kappa_i \to \lambda \kappa_i
}}
{{axiom | n = \text {ECO} 2
        | t = For some $\lambda$, add $\lambda$ times column $j$ to column $i$
        | m = \kappa_i \to \kappa_i + \lambda \kappa_j
}}
{{axiom | n = \text {ECO} 3
        | t = Exchange columns $i$ and $j$
        | m = \kappa_i \leftrightarrow \kappa_j
}}
{{end-axiom}}
Applying $\text {ECO} 1$ has the effect of multiplying $\map \det {\mathbf A}$ by $\lambda$.
Applying $\text {ECO} 2$ has no effect on $\map \det {\mathbf A}$.
Applying $\text {ECO} 3$ has the effect of multiplying $\map \det {\mathbf A}$ by $-1$.

Proof:
From Elementary Column Operations as Matrix Multiplications, an elementary column operation on $\mathbf A$ is equivalent to matrix multiplication by the elementary column matrices corresponding to the elementary column operations.
From Determinant of Elementary Column Matrix, the determinants of those elementary column matrices are as follows: