avewright/proofwiki-math huggingface dataset:
Theorem: Equivalence of Definitions of Closed Set in Metric Space

{{TFAE|def = Closed Set (Metric Space)|view = Closed Set|context = Metric Space|contextview = Metric Spaces}}
Let $M = \struct {A, d}$ be a metric space.
Let $H \subseteq A$.

Proof:
Let $H'$ denote the set of limit points of $H$.
Theorem: Set of Literals Satisfiable iff No Complementary Pairs

Let $S$ be a set of literals.
Then $S$ is satisfiable {{iff}} it contains no complementary pairs.

Proof:
=== Necessary Condition ===
Suppose $S$ contained the complementary pair $\set {p, \neg p}$.
By the Principle of Non-Contradiction, $\set {p, \neg p}$ is unsatisfiable.
By Superset of Unsatisfiable Set is Unsatisfiable, so is $S$.
Hence if $S$ is satisfiable, it cannot contain any complementary pairs.
{{qed|lemma}}
Theorem: Equivalence of Definitions of Exterior Point (Complex Analysis)

{{TFAE|def = Exterior Point (Complex Analysis)|view = exterior point|context = Complex Analysis}}
Let $S \subseteq \C$ be a subset of the complex plane.
Let $z_0 \in \C$.

Proof:
Let $S \subseteq \C$.
Theorem: Bolzano-Weierstrass Theorem/General Form

Every infinite bounded space in a real Euclidean space has at least one limit point.

Proof:
The proof of this theorem will be given as a series of lemmata that culminate in the actual theorem in the end.
Unless otherwise stated, all real spaces occurring in the proofs are equipped with the Euclidean metric and its related Euclidean topology.
Theorem: Quintuple Angle Formulas/Sine/Corollary

For all $\theta$ such that $\theta \ne 0, \pm \pi, \pm 2 \pi \ldots$
:$\dfrac {\sin 5 \theta} {\sin \theta} = 16 \cos^4 \theta - 12 \cos^2 \theta + 1$
where $\sin$ denotes sine and $\cos$ denotes cosine.

Proof:
First note that when $\theta = 0, \pm \pi, \pm 2 \pi \ldots$:
:$\sin \theta = 0$
so $\dfrac {\sin 5 \theta} {\sin \theta}$ is undefined.
Therefore for the rest of the proof it is assumed that $\theta \ne 0, \pm \pi, \pm 2 \pi \ldots$
{{begin-eqn}}
{{eqn | l = \sin 5 \theta
      | r = 5 \sin \theta - 20 \sin^3 \theta + 16 \sin^5 \theta
      | c = Quintuple Angle Formula for Sine
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\sin 5 \theta} {\sin \theta}
      | r = 5 - 20 \paren {1 - \cos^2 \theta} + 16 \paren {1 - \cos^2 \theta}^2
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = 16 \cos^4 \theta - 12 \cos^2 \theta + 1
      | c = multiplying out and gathering terms
}}
{{end-eqn}}
{{qed}}
Theorem: Complex Multiplication as Geometrical Transformation

Let $z_1 = \left\langle{r_1, \theta_1}\right\rangle$ and $z_2 = \left\langle{r_2, \theta_2}\right\rangle$ be complex numbers expressed in polar form.
Let $z_1$ and $z_2$ be represented on the complex plane $\C$ in vector form.
Let $z = z_1 z_2$ be the product of $z_1$ and $z_2$.
Then $z$ can be interpreted as the result of:
: rotating $z_1$ about the origin of $\C$ by $\theta_2$ in the positive direction
: multiplying the modulus of $z_1$ by $r_2$.

Proof:
:500px
Let $z = r e^{i \alpha}$.
By Product of Complex Numbers in Exponential Form:
:$z = r_1 r_2 e^{i \left({\theta_1 + \theta_2}\right)}$
Adding $\theta_2$ to $\theta_1$ is equivalent to rotation about the origin of $\C$ by $\theta_2$ in the positive direction.
Similarly, the modulus of $z$ is obtained by multiplying the modulus of $z_1$ by $r_2$.
{{qed}}
Theorem: Argument of Quotient equals Difference of Arguments

Let $z_1$ and $z_2$ be complex numbers.
Then:
:$\map \arg {\dfrac {z_1} {z_2} } = \map \arg {z_1} - \map \arg {z_1} + 2 k \pi$
where:
:$\arg$ denotes the argument of a complex number
:$k$ can be $0$, $1$ or $-1$.

Proof:
Let $z_1$ and $z_2$ be expressed in polar form.
:$z_1 = \polar {r_1, \theta_1}$
:$z_2 = \polar {r_2, \theta_2}$
From Division of Complex Numbers in Polar Form:
:$\dfrac {z_1} {z_2} = \dfrac {r_1} {r_2} \paren {\map \cos {\theta_1 - \theta_2} + i \, \map \sin {\theta_1 - \theta_2} }$
By the definition of argument:
:$\map \arg {z_1} = \theta_1$
:$\map \arg {z_2} = \theta_2$
:$\map \arg {\dfrac {z_1} {z_2} } = \theta_1 - \theta_2$
There are $3$ possibilities for the size of $\theta_1 + \theta_2$:
:$(1): \quad \theta_1 - \theta_2 > \pi$
Then:
:$-\pi < \theta_1 - \theta_2 - 2 \pi \le \pi$
and we have:
{{begin-eqn}}
{{eqn | l = \map \cos {\theta_1 - \theta_2}
      | r = \map \cos {\theta_1 - \theta_2 - 2 \pi}
      | c = Cosine of Angle plus Full Angle
}}
{{eqn | l = \map \sin {\theta_1 - \theta_2}
      | r = \map \sin {\theta_1 - \theta_2 - 2 \pi}
      | c = Sine of Angle plus Full Angle
}}
{{end-eqn}}
and so $\theta_1 + \theta_2 - 2 \pi$ is the argument of $\dfrac {z_1} {z_2}$ within its principal range.
:$(2): \quad \theta_1 - \theta_2 \le -\pi$
Then:
:$-\pi < \theta_1 - \theta_2 + 2 \pi \le \pi$
and we have:
{{begin-eqn}}
{{eqn | l = \map \cos {\theta_1 - \theta_2}
      | r = \map \cos {\theta_1 - \theta_2 + 2 \pi}
      | c = Cosine of Angle plus Full Angle
}}
{{eqn | l = \map \sin {\theta_1 - \theta_2}
      | r = \map \sin {\theta_1 - \theta_2 + 2 \pi}
      | c = Sine of Angle plus Full Angle
}}
{{end-eqn}}
and so $\theta_1 - \theta_2 + 2 \pi$ is within the principal range of $\dfrac {z_1} {z_2}$.
:$(3): \quad -\pi < \theta_1 + \theta_2 \le \pi$
Then $\theta_1 - \theta_2$ is already within the principal range of $\dfrac {z_1} {z_2}$.
{{qed}}
Theorem: Conditions on Rational Solution to Polynomial Equation

Let $P$ be the polynomial equation:
:$a_n z^n + a_{n - 1} z^{n - 1} + \cdots + a_1 z + a_0 = 0$
where $a_0, \ldots, a_n$ are integers.
Let $\dfrac p q$ be a root of $P$ expressed in canonical form.
Then $p$ is a divisor of $a_0$ and $q$ is a divisor of $a_n$.

Proof:
By definition of the canonical form of a rational number, $p$ and $q$ are coprime.
Substitute $\dfrac p q$ for $z$ in $P$ and multiply by $q^n$:
:$(1): \quad a_n p^n + a_{n - 1} p^{n - 1} q + \cdots + a_1 p q^{n - 1} + a_0 q^n = 0$
Dividing $(1)$ by $p$ gives:
:$(2): \quad a_n p^{n - 1} + a_{n - 1} p^{n - 2} q + \cdots + a_1 q^{n - 1} = -\dfrac {a_0 q^n} p$
The {{LHS}} of $(2)$ is an integer and therefore so is the {{RHS}}.
We have that $p$ and $q$ are coprime.
By Euclid's Lemma it follows that $p$ divides $a_0$.
Similarly, dividing $(1)$ by $q$ gives:
:$(3): \quad -\dfrac {a_n p^n} q = a_{n - 1} p^{n - 1} + \cdots + a_1 p q^{n - 2} + a_0 q^{n - 1}$
By Euclid's Lemma it follows that $q$ divides $a_n$.
{{qed}}
Theorem: Cardinality of Finite Vector Space

Let $K$ be a Galois field.
Let $V$ be a $K$-vector space.
Let the dimension of $V$ be finite.
Then:
:$\size V = \size K^{\map \dim V}$

Proof:
By Isomorphism from $\R^n$ via $n$-Term Sequence, $V$ is isomorphic to the $K$-vector space $K^{\map \dim V}$.
Thus:
:$\size V = \size {K^{\map \dim V} }$
By Cardinality of Finite Cartesian Space:
:$\size {K^{\map \dim V} } = \size K^{\map \dim V}$
Thus:
:$\size V = \size K^{\map \dim V}$
{{qed}}
Category:Vector Spaces
r5uul1emfje6bozjgy02gdptlpf62b2
Theorem: Sum of Roots of Polynomial

Let $P$ be the polynomial equation:
: $a_n z^n + a_{n - 1} z^{n - 1} + \cdots + a_1 z + a_0 = 0$
such that $a_n \ne 0$.
The sum of the roots of $P$ is $-\dfrac {a_{n - 1} } {a_n}$.

Proof:
Let the roots of $P$ be $z_1, z_2, \ldots, z_n$.
Then $P$ can be written in factored form as:
:$\ds a_n \prod_{k \mathop = 1}^n \paren {z - z_k} = a_n \paren {z - z_1} \paren {z - z_2} \cdots \paren {z - z_n}$
Using Viète's Formulas, $P$ can be expressed as:
:$a_n \paren {z^n - \paren {z_1 + z_2 + \cdots + z_n} z^{n - 1} + \cdots + \paren {-1}^n z_1 z_2 \cdots z_n} = 0$
where the coefficients of $z^{n - 2}, z^{n - 3}, \ldots$ are more complicated and irrelevant.
Equating powers of $z$, it follows that:
:$-a_n \paren {z_1 + z_2 + \cdots + z_n} = a_{n - 1}$
from which:
:$z_1 + z_2 + \cdots + z_n = - \dfrac {a_{n - 1} } {a_n}$
{{qed}}
Theorem: Sum of Roots of Polynomial

Let $P$ be the polynomial equation:
: $a_n z^n + a_{n - 1} z^{n - 1} + \cdots + a_1 z + a_0 = 0$
such that $a_n \ne 0$.
The sum of the roots of $P$ is $-\dfrac {a_{n - 1} } {a_n}$.

Proof:
From Viète's Formulas:
:$\ds a_{n - k} = \paren {-1}^k a_n \sum_{1 \mathop \le i_1 \mathop < \dotsb \mathop < i_k \mathop \le n} z_{i_1} \dotsm z_{i_k}$
for $k = 1, 2, \ldots, n$.
The result follows for $k = 1$.
{{qed}}
Theorem: Sum of Roots of Polynomial

Let $P$ be the polynomial equation:
: $a_n z^n + a_{n - 1} z^{n - 1} + \cdots + a_1 z + a_0 = 0$
such that $a_n \ne 0$.
The sum of the roots of $P$ is $-\dfrac {a_{n - 1} } {a_n}$.

Proof:
Proof by induction.
For $n \in \N_{> 0}$, let $\map S n$ be the statement:
:For polynomial $P$ of degree $n$, the sum of the roots of $P$ is $-\dfrac {a_{n - 1} } {a_n}$.
=== Basis of Induction ===
Let $P$ be the polynomial of degree $1$:
:$\map P x = a_0 + a_1 z$
The single root of $P$ is:
:$a_0 + a_1 z = 0 \implies z = -\dfrac {a_0} {a_1}$
So, $\map S 1$ is true.
{{qed|lemma}}
=== Induction Hypothesis ===
Now we must show that $\map S k \implies \map S {k + 1}$ for all $k \geq 1$.
That is, we assume the induction hypothesis:
:For polynomial $P$ of degree $k$, the sum of the roots of $P$ is $-\dfrac {a_{k - 1} } {a_k}$.
in order to prove that:
:For polynomial $P$ of degree $k + 1$, the sum of the roots of $P$ is $-\dfrac {a_k} {a_{k + 1} }$.
=== Induction Step ===
Let $P$ be a polynomial of degree $k + 1$.
Let $\lambda$ be a root of $P$.
Then, by the Polynomial Factor Theorem, $P$ can be written as:
:$\map P z = \paren {z - \lambda} \map Q x$
where $Q$ is a polynomial of degree $k$.
Let $Q$ be written as:
:$\ds \sum_{i \mathop = 0}^k b_i z^i$
We can now write $\map P z$ as
{{begin-eqn}}
{{eqn | l = \map P z
      | r = \paren {z - \lambda} \map Q x 
}}
{{eqn | r = \paren {z - \lambda} \sum_{i \mathop = 0}^k b_i z^i
}}
{{eqn | r = z \sum_{i \mathop = 0}^k b_i z^i - \lambda \sum_{i \mathop = 0}^k b_i z^i
      | c = Multiplication Distributes over Addition
}}
{{eqn | r = \sum_{i \mathop = 0}^k b_i z^{i + 1} - \sum_{i \mathop = 0}^k \lambda b_i z^i
      | c = Indexed Summation of Multiple of Mapping
}}
{{eqn | r = b_k z^{k + 1} + \sum_{i \mathop = 0}^{k - 1} b_i z^{i + 1} - \sum_{i \mathop = 1}^k \lambda b_i z^i - \lambda b_0
}}
{{eqn | r = b_k z^{k + 1} + \sum_{i \mathop = 1}^k b_{i - 1} z^i - \sum_{i \mathop = 1}^k \lambda b_i z^i - \lambda b_0
      | c = {{Corollary|Translation of Index Variable of Summation}}
}}
{{eqn | r = b_k z^{k + 1} + \sum_{i \mathop = 1}^k \paren {b_{i - 1} z^i - \lambda b_i z^i} - \lambda b_0
      | c = Indexed Summation of Sum of Mappings
}}
{{eqn | r = b_k z^{k + 1} + \sum_{i \mathop = 1}^k \paren {b_{i - 1} - \lambda b_i} z^i - \lambda b_0
      | c = Multiplication Distributes over Addition
}}
{{end-eqn}}
So, by matching up exponents of $z$:
:$a_{k + 1} = b_k$
and:
:$a_k = b_{k - 1} - \lambda b_k$.
Therefore:
{{begin-eqn}}
{{eqn | l = -\frac {a_k} {a_{k + 1} }
      | r = -\frac {b_{k - 1} - \lambda b_k} {b_k}
}}
{{eqn | r = -\frac {b_{k - 1} } {b_k} + \lambda
}}
{{end-eqn}}
By the induction hypothesis, the sum of the roots of $Q$ is $-\dfrac {b_{k - 1} } {b_k}$.
Since every root of $Q$ is a root of $P$, the final expression is the sum of the roots of $P$.
So, the sum of the roots of $P$ is $-\dfrac {a_k} {a_{k + 1} }$
{{qed|lemma}}
Thus, $\map S n$ holds for all $n \in \N_{> 0}$.
{{qed}}
Theorem: Product of Roots of Polynomial

Let $P$ be the polynomial equation:
:$a_n z^n + a_{n - 1} z^{n - 1} + \cdots + a_1 z + a_0 = 0$
such that $a_n \ne 0$.
The product of the roots of $P$ is $\dfrac {\paren {-1}^n a_0} {a_n}$.

Proof:
Let the roots of $P$ be $z_1, z_2, \ldots, z_n$.
Then $P$ can be written in factored form as:
:$\ds a_n \prod_{k \mathop = 1}^n \paren {z - z_k} = a_0 \paren {z - z_1} \paren {z - z_2} \dotsm \paren {z - z_n}$
From Viète's Formulas, $P$ can be expressed as:
:$a_n \paren {z^n - \paren {z_1 + z_2 + \dotsb + z_n} z^{n - 1} + \dotsb + \paren {-1}^n z_1 z_2 \dotsm z_n} = 0$
where the coefficients of $z^{n - 2}, z^{n - 3}, \ldots$ are more complicated and irrelevant.
Equating powers of $z$, it follows that:
:$a_n \paren {-1}^n z_1 z_2 \dotsm z_n = a_0$
from which:
:$z_1 z_2 \dotsm z_n = \dfrac {\paren {-1}^n a_0} {a_n}$
{{qed}}
Theorem: Sum of Cosines of Fractions of Pi

Let $n \in \Z$ such that $n > 1$.
Then:
:$\ds \sum_{k \mathop = 1}^{n - 1} \cos \frac {2 k \pi} n = -1$

Proof:
Consider the equation:
:$z^n - 1 = 0$
whose solutions are the complex roots of unity:
:$1, e^{2 \pi i / n}, e^{4 \pi i / n}, e^{6 \pi i / n}, \ldots, e^{2 \paren {n - 1} \pi i / n}$
By Sum of Roots of Polynomial:
:$1 + e^{2 \pi i / n} + e^{4 \pi i / n} + e^{6 \pi i / n} + \cdots + e^{2 \paren {n - 1} \pi i / n} = 0$
From Euler's Formula:
:$e^{i \theta} = \cos \theta + i \sin \theta$
from which comes:
:$\paren {1 + \cos \dfrac {2 \pi} n + \cos \dfrac {4 \pi} n + \cdots + \cos \dfrac {2 \paren {n - 1} \pi} n} + i \paren {\sin \dfrac {2 \pi} n + \sin \dfrac {4 \pi} n + \cdots + \sin \dfrac {2 \paren {n - 1} \pi} n} = 0$
Equating real parts:
:$1 + \cos \dfrac {2 \pi} n + \cos \dfrac {4 \pi} n + \cdots + \cos \dfrac {2 \paren {n - 1} \pi} n = 0$
whence the result.
{{qed}}
Theorem: Sum of Sines of Fractions of Pi

:$\forall n \in \Z_{>1}: \ds \sum_{k \mathop = 1}^{n - 1} \sin \frac {2 k \pi} n = 0$

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 1}^{n - 1} \sin \frac {2 k \pi} n
      | r = \sin \frac {2 \paren 1 \pi} n + \sin \frac {2 \paren 2 \pi} n + \sin \frac {2 \paren 3 \pi} n + \cdots + \sin \frac {2 \paren {n - 3} \pi} n + \sin \frac {2 \paren {n - 2} \pi} n + \sin \frac {2 \paren {n - 1} \pi} n  
      | c = 
}}
{{eqn | r = \paren {\sin \frac {2 \paren 1 \pi} n + \sin \frac {2 \paren {n - 1} \pi} n } + \paren {\sin \frac {2 \paren 2 \pi} n + \sin \frac {2 \paren {n - 2} \pi} n } + \paren {\sin \frac {2 \paren 3 \pi} n + \sin \frac {2 \paren {n - 3} \pi} n } + \cdots
      | c = regrouping
}}
{{eqn | r = \paren {\sin \frac {2 \paren 1 \pi} n + \map \sin {2 \pi + \frac {2 \paren {- 1} \pi} n } } + \paren {\sin \frac {2 \paren 2 \pi} n + \map \sin {2 \pi + \frac {2 \paren {- 2} \pi} n } } + \paren {\sin \frac {2 \paren 3 \pi} n + \map \sin {2 \pi + \frac {2 \paren {- 3} \pi} n } } + \cdots
      | c = 
}}
{{eqn | r = \paren {\sin \frac {2 \paren 1 \pi} n - \sin \frac {2 \paren 1 \pi} n } + \paren {\sin \frac {2 \paren 2 \pi} n - \sin \frac {2 \paren 2 \pi} n } + \paren {\sin \frac {2 \paren 3 \pi} n - \sin \frac {2 \paren 3 \pi} n } + \cdots
      | c = Sine of Angle plus Full Angle and Sine Function is Odd
}}
{{eqn | r = \paren 0 + \paren 0 + \paren 0 + \cdots
      | c = 
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
When $n$ is odd, the number of terms in the sum will be even and every $\map \sin {\dfrac {2 \paren k \pi} n}$ will have a corresponding $-\map \sin {\dfrac {2 \paren k \pi} n }$.
When $n$ is even, the number of terms in the sum will be odd and one term will not have an additive inverse.
When $n = 2 r$, this lone term will be at $k = r$
:$\ds \map \sin {\dfrac {2 \paren r \pi} {2 r} } = \map \sin {\pi } = 0$
{{qed}}
Theorem: Area of Parallelogram in Complex Plane

Let $z_1$ and $z_2$ be complex numbers expressed as vectors.
Let $ABCD$ be the parallelogram formed by letting $AD = z_1$ and $AB = z_2$.
Then the area $\AA$ of $ABCD$ is given by:
:$\AA = z_1 \times z_2$
where $z_1 \times z_2$ denotes the cross product of $z_1$ and $z_2$.

Proof:
:400px
From Area of Parallelogram:
:$\AA = \text{base} \times \text{height}$
In this context:
:$\text {base} = \cmod {z_2}$
and:
:$\text {height} = \cmod {z_1} \sin \theta$
The result follows by definition of complex cross product.
{{qed}}
Theorem: Area of Triangle in Determinant Form

Let $A = \tuple {x_1, y_1}, B = \tuple {x_2, y_2}, C = \tuple {x_3, y_3}$ be points in the Cartesian plane.
The area $\AA$ of the triangle whose vertices are at $A$, $B$ and $C$ is given by:
:$\AA = \dfrac 1 2 \size {\paren {\begin {vmatrix} x_1 & y_1 & 1 \\ x_2 & y_2 & 1 \\ x_3 & y_3 & 1 \\ \end {vmatrix} } }$

Proof:
{{begin-eqn}}
{{eqn | l = \map \Area T
      | r = \dfrac 1 2 \size {\paren {\begin {vmatrix} 0 & 0 & 1 \\ b & a & 1 \\ x & y & 1 \end {vmatrix} } }
      | c = Area of Triangle in Determinant Form
}}
{{eqn | r = \dfrac 1 2 \size {b y - a x}
      | c = Determinant of Order 3
}}
{{end-eqn}}
{{qed}}
Theorem: Area of Triangle in Determinant Form

Let $A = \tuple {x_1, y_1}, B = \tuple {x_2, y_2}, C = \tuple {x_3, y_3}$ be points in the Cartesian plane.
The area $\AA$ of the triangle whose vertices are at $A$, $B$ and $C$ is given by:
:$\AA = \dfrac 1 2 \size {\paren {\begin {vmatrix} x_1 & y_1 & 1 \\ x_2 & y_2 & 1 \\ x_3 & y_3 & 1 \\ \end {vmatrix} } }$

Proof:
Let the polar coordinates of $B$ and $C$ be:
{{begin-eqn}}
{{eqn | l = B
      | r = \polar {r_1, \theta_1}
}}
{{eqn | l = C
      | r = \polar {r_2, \theta_2}
}}
{{end-eqn}}
Let $\theta$ be the angle between $AB$ and $AC$.
Then we have:
{{begin-eqn}}
{{eqn | l = \map \Area {\triangle ABC}
      | r = \dfrac 1 2 AB \cdot AC \sin \theta
      | c = Area of Triangle in Terms of Two Sides and Angle
}}
{{eqn | r = \dfrac 1 2 r_1 r_2 \map \sin {\theta_2 - \theta_1}
      | c = Definition of $\theta$
}}
{{eqn | r = \dfrac 1 2 r_1 r_2 \paren {\sin \theta_2 \cos \theta_1 - \cos \theta_2 \sin \theta_1}
      | c = Sine of Difference
}}
{{eqn | r = \dfrac 1 2 \paren {r_1 \cos \theta_1 r_2 \sin \theta_2 - r_1 \sin \theta_1 r_2 \cos \theta_2}
      | c = rearranging
}}
{{eqn | r = \dfrac 1 2 \paren {b y - a x}
      | c = rearranging
}}
{{end-eqn}}
We can define the area of $\triangle ABC$ as being positive or negative according to the sign of $\dfrac 1 2 \paren {b y - a x}$.
However, if we are interested only in the absolute value of $\triangle ABC$, as in this context, we can report:
:$\map \Area {\triangle ABC} = \dfrac {\size {b y - a x} } 2$
{{qed}}
Theorem: Area of Triangle in Determinant Form

Let $A = \tuple {x_1, y_1}, B = \tuple {x_2, y_2}, C = \tuple {x_3, y_3}$ be points in the Cartesian plane.
The area $\AA$ of the triangle whose vertices are at $A$, $B$ and $C$ is given by:
:$\AA = \dfrac 1 2 \size {\paren {\begin {vmatrix} x_1 & y_1 & 1 \\ x_2 & y_2 & 1 \\ x_3 & y_3 & 1 \\ \end {vmatrix} } }$

Proof:
:400px
Let $A$, $B$ and $C$ be defined as complex numbers in the complex plane.
The vectors from $C$ to $A$ and from $C$ to $B$ are given by:
:$z_1 = \paren {x_1 - x_3} + i \paren {y_1 - y_3}$
:$z_2 = \paren {x_2 - x_3} + i \paren {y_2 - y_3}$
From Area of Triangle in Terms of Side and Altitude, $\AA$ is half that of a parallelogram contained by $z_1$ and $z_2$.
Thus:
{{begin-eqn}}
{{eqn | l = \AA
      | r = \frac 1 2 z_1 \times z_2
      | c = Area of Parallelogram in Complex Plane
}}
{{eqn | r = \frac 1 2 \size {\paren {\map \Im {\paren {x_1 - x_3} - i \paren {y_1 - y_3} } \paren {\paren {x_2 - x_3} - i \paren {y_2 - y_3} } } }
      | c = {{Defof|Vector Cross Product|subdef = Complex|index = 3}}
}}
{{eqn | r = \frac 1 2 \size {\paren {x_1 - x_3} \paren {y_2 - y_3} - \paren {y_1 - y_3} \paren {x_2 - x_3} }
      | c = {{Defof|Complex Multiplication}}
}}
{{eqn | r = \frac 1 2 \size {x_1 y_2 - y_1 x_2 + x_2 y_3 - y_2 x_3 + x_3 y_1 - y_3 x_1}
      | c = multiplying out
}}
{{eqn | r = \frac 1 2 \size {\paren {\begin {vmatrix} x_1 & y_1 & 1 \\ x_2 & y_2 & 1 \\ x_3 & y_3 & 1 \\ \end {vmatrix} } }
      | c = Determinant of Order 3
}}
{{end-eqn}}
{{qed}}
Theorem: Area of Triangle in Determinant Form

Let $A = \tuple {x_1, y_1}, B = \tuple {x_2, y_2}, C = \tuple {x_3, y_3}$ be points in the Cartesian plane.
The area $\AA$ of the triangle whose vertices are at $A$, $B$ and $C$ is given by:
:$\AA = \dfrac 1 2 \size {\paren {\begin {vmatrix} x_1 & y_1 & 1 \\ x_2 & y_2 & 1 \\ x_3 & y_3 & 1 \\ \end {vmatrix} } }$

Proof:
:400px
Let $A$, $B$ and $C$ be as defined..
Let $O$ be the origin of the Cartesian plane in which $\triangle ABC$ is embedded.
Taking into account the signs of the areas of the various triangles involved:
:$\triangle ABC = \triangle OAB + \triangle OBC + \triangle OCA$
as it is seen that $\triangle OBC$ and $\triangle OCA$ are described in clockwise sense.
From proof 2 of Area of Triangle in Determinant Form with Vertex at Origin:
{{begin-eqn}}
{{eqn | l = \triangle OAB
      | r = \dfrac 1 2 \paren {x_1 y_2 - x_2 y_1}
}}
{{eqn | l = \triangle OBC
      | r = \dfrac 1 2 \paren {x_2 y_3 - x_3 y_2}
}}
{{eqn | l = \triangle OBC
      | r = \dfrac 1 2 \paren {x_3 y_1 - x_1 y_3}
}}
{{eqn | ll= \leadsto
      | l = \triangle ABC
      | r = \dfrac 1 2 \paren {\paren {x_1 y_2 - x_2 y_1} + \paren {x_2 y_3 - x_3 y_2} + \paren {x_3 y_1 - x_1 y_3} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \triangle ABC
      | r = \frac 1 2 \paren {\begin {vmatrix} x_1 & y_1 & 1 \\ x_2 & y_2 & 1 \\ x_3 & y_3 & 1 \\ \end {vmatrix} }
      | c = Determinant of Order 3
}}
{{end-eqn}}
The result follows.
{{qed}}
Theorem: Area of Triangle in Determinant Form

Let $A = \tuple {x_1, y_1}, B = \tuple {x_2, y_2}, C = \tuple {x_3, y_3}$ be points in the Cartesian plane.
The area $\AA$ of the triangle whose vertices are at $A$, $B$ and $C$ is given by:
:$\AA = \dfrac 1 2 \size {\paren {\begin {vmatrix} x_1 & y_1 & 1 \\ x_2 & y_2 & 1 \\ x_3 & y_3 & 1 \\ \end {vmatrix} } }$

Proof:
:400px
Let $A$, $B$ and $C$ be defined as $\tuple {x_1, y_1}$, $\tuple {x_2, y_2}$ and $\tuple {x_3, y_3}$ respectively.
From the figure, we see that:
{{begin-eqn}}
{{eqn | l = \map \Area {ABC}
      | r = \map \Area {PACR} + \map \Area {RCBQ} - \map \Area {PABQ}
      | c = 
}}
{{eqn | r = \dfrac {\paren {x_3 - x_1} \paren {y_3 + y_1} } 2 + \dfrac {\paren {x_2 - x_3} \paren {y_2 + y_3} } 2 - \dfrac {\paren {x_2 - x_1} \paren {y_1 + y_2} } 2
      | c = Area of Trapezium
}}
{{eqn | r = \dfrac {x_1 y_2 - x_2 y_1 + x_2 y_3 - x_3 y_2 + x_3 y_1 - x_1 y_3} 2
      | c = simplification
}}
{{eqn | r = \dfrac 1 2 \size {\paren {\begin {vmatrix}  x_1 & y_1 & 1 \\ x_2 & y_2 & 1 \\ x_3 & y_3 & 1 \\ \end {vmatrix} } }
      | c = Determinant of Order 3
}}
{{end-eqn}}
{{qed}}
Theorem: Equation of Circle in Complex Plane/Formulation 2

Let $\C$ be the complex plane.
Let $C$ be a circle in $\C$.
Then $C$ may be written as:
:$\alpha z \overline z + \beta z + \overline \beta \overline z + \gamma = 0$
where:
:$\alpha \in \R_{\ne 0}$ is real and non-zero
:$\gamma \in \R$ is real
:$\beta \in \C$ is complex such that $\cmod \beta^2 > \alpha \gamma$.
The curve $C$ is a straight line {{iff}} $\alpha = 0$ and $\beta \ne 0$.

Proof:
{{begin-eqn}}
{{eqn | l = \cmod {z - a}
      | r = r
      | c = Equation of Circle in Complex Plane: Formulation 1
}}
{{eqn | ll= \leadsto
      | l = \cmod {z - a}^2
      | r = r^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {z - a} \overline {\paren {z - a} }
      | r = r^2
      | c = Modulus in Terms of Conjugate
}}
{{eqn | ll= \leadsto
      | l = \paren {z - a} {\paren {\overline z - \overline a} }
      | r = r^2
      | c = Sum of Complex Conjugates
}}
{{eqn | ll= \leadsto
      | l = z \overline z - a z - \overline a \overline z + a \overline a
      | r = r^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \alpha z \overline z - \alpha a z - \alpha \overline a \overline z + \alpha a \overline a - r^2
      | r = 0
      | c = where $\alpha \in \R_{>0}$ is arbitrary
}}
{{end-eqn}}
By setting:
: $\beta := -\alpha a$ and $\gamma = \alpha a \overline a - r^2$
we have:
:$\alpha z \overline z + \beta z + \overline \beta \overline z + \gamma = 0$
We have that:
{{begin-eqn}}
{{eqn | l = r^2
      | o = >
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \alpha a \overline a - \gamma
      | o = >
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {\alpha a} \paren {\alpha \overline a}
      | o = >
      | r = \alpha \gamma
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \beta \overline \beta 
      | o = >
      | r = \alpha \gamma
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \cmod {\beta}^2
      | o = >
      | r = \alpha \gamma
      | c = Modulus in Terms of Conjugate
}}
{{end-eqn}}
{{qed|lemma}}
If $\alpha = 0$ and $\beta \ne 0$ the equation devolves to:
:$\beta z + \overline \beta \overline z + \gamma = 0$
which from Equation of Line in Complex Plane: Formulation 1 is the equation of a straight line.
The result follows.
{{qed}}