avewright/proofwiki-math huggingface dataset:
Theorem: Sample Mean is Unbiased Estimator of Population Mean

Let $X_1, X_2, \ldots, X_n$ form a random sample from a population with mean $\mu$ and variance $\sigma^2$.
Then: 
:$\ds \bar X = \frac 1 n \sum_{i \mathop = 1}^n X_i$
is an unbiased estimator of $\mu$.

Proof:
If $\bar X$ be an unbiased estimator of $\mu$, then: 
:$\expect {\bar X} = \mu$
{{Explain|The structure of this proof is confusing. It starts with what looks like an assertion of what we are trying to prove.}}
We have: 
{{begin-eqn}}
{{eqn | l = \expect {\bar X}
      | r = \expect {\frac 1 n \sum_{i \mathop = 1}^n X_i}
}}
{{eqn | r = \frac 1 n \sum_{i \mathop = 1}^n \expect {X_i}
      | c = Expectation is Linear
}}
{{eqn | r = \frac 1 n \sum_{i \mathop = 1}^n \mu
      | c = as $\expect {X_i} = \mu$
}}
{{eqn | r = \frac n n \mu
      | c = as $\ds \sum_{i \mathop = 1}^n 1 = n$
}}
{{eqn | r = \mu
}}
{{end-eqn}}
So $\bar X$ is an unbiased estimator of $\mu$. 
{{qed}}
Theorem: Ostrowski's Theorem/Archimedean Norm

Let $\norm {\, \cdot \,}$ be a non-trivial Archimedean norm on the rational numbers $\Q$.
Then $\norm {\, \cdot \,}$ is equivalent to the absolute value $\size {\, \cdot \,}$.

Proof:
By Characterisation of Non-Archimedean Division Ring Norms then:
:$\exists n \in \N$ such that $\norm n > 1$
Let $n_0 = \min \set {n \in \N : \norm n > 1}$
By Norm of Unity then:
:$n_0 > 1$
Let $\alpha = \dfrac {\log \norm {n_0} } {\log n_0}$
Since $n_0, \norm n_0 > 1$ then:
:$\alpha > 0$
==== Lemma 1.1 ====
{{:Ostrowski's Theorem/Archimedean Norm/Lemma 1.1}}{{qed|lemma}}
==== Lemma 1.2 ====
{{:Ostrowski's Theorem/Archimedean Norm/Lemma 1.2}}{{qed|lemma}}
Hence:
:$\forall n \in \N: \norm n = n^\alpha = \size n^\alpha$
By Equivalent Norms on Rational Numbers then $\norm {\, \cdot \,}$ is equivalent to the absolute value $\size {\, \cdot \,}$.
Theorem: Ostrowski's Theorem/Non-Archimedean Norm

Let $\norm {\, \cdot \,}$ be a non-trivial non-Archimedean norm on the rational numbers $\Q$.
Then $\norm {\, \cdot \,}$ is equivalent to the $p$-adic norm $\norm {\, \cdot \,}_p$ for some prime $p$.

Proof:
From Characterisation of Non-Archimedean Division Ring Norms:
:$\forall n \in \N: \norm n \le 1$
==== Lemma 2.1 ====
{{:Ostrowski's Theorem/Non-Archimedean Norm/Lemma 2.1}}{{qed|lemma}}
Let $n_0 = \min \set {n \in N : \norm n < 1}$.
==== Lemma 2.2 ====
{{:Ostrowski's Theorem/Non-Archimedean Norm/Lemma 2.2}}{{qed|lemma}}
Let $p = n_0$.
Let $\alpha = - \dfrac {\log \norm p } {\log p}$ then:
:$\norm p = p^{-\alpha} = \paren {p^{-1}}^\alpha = \norm p_p^\alpha$
Let $b \in \N$.
=== Case 1: $p \nmid b$ ===
Let $p \nmid b$.
From Prime not Divisor implies Coprime:
:$p$ and $b$ are coprime, that is, $p \perp b$
From {{Corollary|Three Points in Ultrametric Space have Two Equal Distances|5}}:
:$\norm b = 1$
By the definition of the $p$-adic norm:
:$\norm b_p = 1$ 
Hence:
:$\norm b = 1 = 1^\alpha = \norm b_p^\alpha$
{{qed|lemma}}
=== Case 2: $p \divides b$ ===
Let $p \divides b$.
Let $\nu = \map {\nu_p} b$ where $\nu_p$ is the $p$-adic valuation on $\Z$.
Then:
:$b = p^\nu c$
where $p \nmid c$
From Case 1:
:$\norm c = 1$
Hence:
{{begin-eqn}}
{{eqn | l = \norm b
      | r = \norm p^\nu \norm {c}
      | c = {{NormAxiomNonArch|2}}
}}
{{eqn | r = \norm p^\nu
      | c = 
}}
{{eqn | r = \norm p_p^{\alpha \nu}
}}
{{eqn | r = \paren {p^{-1} }^{\alpha \nu}
      | c = {{Defof|P-adic Norm|$p$-adic Norm}}
}}
{{eqn | r = p^{-\alpha \nu}
      | c = 
}}
{{eqn | r = \paren {p^{-\nu} }^\alpha
      | c = 
}}
{{eqn | r = \norm b_p^\alpha
      | c = {{Defof|P-adic Norm|$p$-adic Norm}}
}}
{{end-eqn}}
{{qed|lemma}}
In either case:
:$\norm b = \norm b_p^\alpha$
Since $b$ was arbitrary, it has been shown:
:$\forall b \in \N: \norm b = \norm b_p^\alpha$
From Equivalent Norms on Rational Numbers:
:$\norm {\, \cdot \,}$ is equivalent to the $p$-adic norm $\norm {\, \cdot \,}_p$.
Theorem: Ostrowski's Theorem/Archimedean Norm/Lemma 1.1

:$\forall n \in N: \norm n \le n^\alpha$

Proof:
By the definition of $\alpha$ then:
:$\norm {n_0} = {n_0}^\alpha$
By the definition of $n_0$ then:
:${n_0}^\alpha > 1$
Let $n \in \N$.
By Basis Representation Theorem then $n$ can be written:
:$n = a_0 + a_1 n_0 + a_2 {n_0}^2 + \cdots + a_s {n_0}^s$
where $0 \le a_i < n_0$ and $a_s \ne 0$
Since all of the $a_i < n_0$, by choice of $n_0$ then:
:$\forall a_i: \norm {a_i} \le 1$
Then:
{{begin-eqn}}
{{eqn | l = \norm n
      | o = \le
      | r = \norm {a_0} + \norm {a_1 n_0} + \norm {a_2 {n_0}^2} + \cdots + \norm {a_s {n_0}^s}
      | c = {{Norm-axiom-mult|3}}
}}
{{eqn | r = \norm {a_0} + \norm {a_1} \norm {n_0} + \norm {a_2} \norm {n_0}^2 + \cdots + \norm {a_s} \norm {n_0}^s
      | c = {{Norm-axiom-mult|2}}
}}
{{eqn | r = \norm {a_0} + \norm {a_1} n_0^\alpha + \norm {a_2} {n_0}^{2 \alpha} + \cdots + \norm {a_s} {n_0}^{s\alpha}
      | c = as $\norm {n_0} = {n_0}^\alpha$
}}
{{eqn | o = \le
      | r = 1 + {n_0}^\alpha + {n_0}^{2 \alpha} + \cdots + {n_0}^{s \alpha}
      | c = as $\forall a_i: \norm {a_i} \le 1$
}}
{{eqn | r = n_0^{s \alpha} \paren {1 + {n_0}^{-\alpha} + {n_0}^{-2 \alpha} + \cdots + {n_0}^{-s \alpha} }
      | c = 
}}
{{eqn | o = \le
      | r = {n_0}^{s \alpha} \paren {\sum_{i \mathop = 0}^\infty \paren {\frac 1 { {n_0}^\alpha} }^i} 
      | c = 
}}
{{eqn | r = {n_0}^{s \alpha} \paren {\dfrac { {n_0}^\alpha} { {n_0}^\alpha - 1} }
      | c = Sum of Infinite Geometric Progression (and as ${n_0}^\alpha > 1$)
}}
{{eqn | o = \le
      | r = n^\alpha \paren {\dfrac { {n_0}^\alpha} { {n_0}^\alpha - 1} }
      | c = as $n \ge {n_0}^s$
}}
{{end-eqn}}
Let $C = \paren {\dfrac { {n_0}^\alpha} { {n_0}^\alpha - 1} }$
Hence:
:$\norm n \le C n^\alpha$
As $n \in \N$ was arbitrary:
:$\forall n \in N: \norm n \le C n^\alpha$
Let $n, N \in N$
Then:
:$\norm {n^N} \le C \paren {n^N}^\alpha$
Now:
{{begin-eqn}}
{{eqn | l = \norm {n^N} \le C \paren {n^N}^\alpha
      | o = \leadsto
      | r = \norm n^N \le C \paren {n^N}^\alpha
      | c = {{Norm-axiom-mult|2}}
}}
{{eqn | o = \leadsto
      | r = \norm n^N \le C \paren {n^\alpha}^N
      | c = 
}}
{{eqn | o = \leadsto
      | r = \norm n \le \sqrt [N] C n^\alpha
      | c = taking $N$th roots
}}
{{end-eqn}}
By Limit of Root of Positive Real Number:
:$\sqrt [N] C \to 1$ as $N \to \infty$
By the Multiple Rule for Real Sequences:
:$\sqrt [N] C n^\alpha \to n^\alpha$ as $N \to \infty$
By Inequality Rule for Real Sequences, letting $N \to \infty$ for fixed $n$:
:$\norm n \le n^\alpha$
The result follows.
{{qed}}
Theorem: Ostrowski's Theorem/Archimedean Norm/Lemma 1.2

:$\forall n \in N: \norm n \ge n^\alpha$

Proof:
By the definition of $\alpha$:
:$\norm {n_0} = {n_0}^\alpha$
By the definition of $n_0$:
:${n_0}^\alpha > 1$
Let $n \in \N$.
By Basis Representation Theorem then $n$ can be written:
:$n = a_0 + a_1 n_0 + a_2 {n_0}^2 + \cdots + a_s {n_0}^s$
where $0 \le a_i < n_0$ and $a_s \ne 0$
By Bounds for Integer Expressed in Base k:
:${n_0}^{s + 1} > n \ge {n_0}^s$
By Lemma 1.1:
:$\norm { {n_0}^{s + 1} - n} \le \paren { {n_0}^{s + 1} - n}^\alpha$
Hence:
{{begin-eqn}}
{{eqn | l = \norm n
      | o = \ge
      | r = \norm { {n_0}^{s + 1} } - \norm { {n_0}^{s + 1} - n}
      | c = Reverse Triangle Inequality on Normed Division Ring
}}
{{eqn | r = \norm {n_0}^{s + 1} - \norm { {n_0}^{s + 1} - n}
      | c = {{Norm-axiom-mult|2}}
}}
{{eqn | r = {n_0}^{\alpha \paren {s + 1} } - \norm { {n_0}^{s + 1} - n}
      | c = as $\norm {n_0} = {n_0}^\alpha$
}}
{{eqn | o = \ge
      | r = {n_0}^{\alpha \paren {s + 1} } - \paren { {n_0}^{s + 1} - n}^\alpha
      | c = as $\norm { {n_0}^{s + 1} - n} \le \paren { {n_0}^{s + 1} - n}^\alpha$
}}
{{eqn | o = \ge
      | r = {n_0}^{\alpha \paren {s + 1} } - \paren { {n_0}^{s + 1} - {n_0}^s}^\alpha
      | c = as $n \ge n_0^s$
}}
{{eqn | r = {n_0}^{\alpha \paren {s + 1} } \paren {1 - \paren {1 - \frac 1 {n_0} }^\alpha}
      | c = 
}}
{{eqn | o = \ge
      | r = n^\alpha \paren {1 - \paren {1 - \frac 1 {n_0} }^\alpha}
      | c = as ${n_0}^{s + 1} > n$
}}
{{end-eqn}}
Let $C' = \paren{1 - \paren{1 - \frac 1 {n_0} }^\alpha}$.
Then:
:$\norm n \ge C' n^\alpha$
As $n \in \N$ was arbitrary:
:$\forall n \in N: \norm n \ge C' n^\alpha$
Let $n, N \in N$.
Then:
:$\norm {n^N} \ge C' \paren {n^N}^\alpha$
Now:
{{begin-eqn}}
{{eqn | l = \norm {n^N} \ge C' \paren {n^N}^\alpha
      | o = \leadsto
      | r = \norm n^N \ge C' \paren {n^N}^\alpha
      | c = {{Norm-axiom-mult|2}}
}}
{{eqn | o = \leadsto
      | r = \norm n^N \ge C' \paren {n^\alpha}^N
      | c = 
}}
{{eqn | o = \leadsto
      | r = \norm n \ge \sqrt [N] {C'} n^\alpha
      | c = taking $N$th roots
}}
{{end-eqn}}
By Limit of Root of Positive Real Number:
:$\sqrt [N] {C'} \to 1$ as $N \to \infty$
By the Multiple Rule for Real Sequences:
:$\sqrt [N] {C'} n^\alpha \to n^\alpha$ as $N \to \infty$
By Inequality Rule for Real Sequences, letting $N \to \infty$ for fixed $n$:
:$\norm n \ge n^\alpha$
The result follows.
{{qed}}
Theorem: Roots of Complex Number/Examples/z^4 + 81 = 0

The roots of the polynomial:
:$z^4 + 81$
are:
:$\set {3 \cis 45 \degrees, 3 \cis 135 \degrees, 3 \cis 225 \degrees, 3 \cis 315 \degrees}$

Proof:
From Factorisation of $z^n + 1$:
:$z^4 + 1 = \ds \prod_{k \mathop = 0}^3 \paren {z - \exp \dfrac {\paren {2 k + 1} i \pi} 4}$
Thus:
:$z = \set {\exp \dfrac {\paren {2 k + 1} i \pi} 4}$
{{begin-eqn}}
{{eqn | n = k = 0
      | l = z
      | r = \cos \dfrac \pi 4 + i \sin \dfrac \pi 4
      | c = 
}}
{{eqn | n = k = 1
      | l = z
      | r = \cos \dfrac {3 \pi} 4 + i \sin \dfrac {3 \pi} 4
      | c = 
}}
{{eqn | n = k = 2
      | l = z
      | r = \cos \dfrac {5 \pi} 4 + i \sin \dfrac {5 \pi} 4
      | c = 
}}
{{eqn | n = k = 3
      | l = z
      | r = \cos \dfrac {7 \pi} 4 + i \sin \dfrac {7 \pi} 4
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Equivalent Norms on Rational Numbers

Let $\norm {\, \cdot \,}_1$ and $\norm {\, \cdot \,}_2$ be norms on the rational numbers $\Q$.
Then $\norm {\, \cdot \,}_1$ and $\norm {\, \cdot \,}_2$ are equivalent {{iff}}:
:$\exists \alpha \in \R_{\gt 0}: \forall n \in \N: \norm n_1 = \norm n_2^\alpha$

Proof:
=== Necessary Condition ===
{{:Equivalent Norms on Rational Numbers/Necessary Condition}}{{qed|lemma}}
Theorem: Ostrowski's Theorem/Non-Archimedean Norm/Lemma 2.1

:$\exists n \in \N: 0 < \norm n < 1$

Proof:
Because $\norm {\, \cdot \,}$ is non-trivial:
:$\exists \dfrac a b \in \Q : 0 < \norm {\dfrac a b} \mbox { and } \norm {\dfrac a b} \ne 1$
By Norm of Inverse:
:$\norm {\dfrac a b} > 1 \implies \norm {\dfrac b a} < 1$
Hence either $\norm {\dfrac a b} < 1$ or $\norm {\dfrac b a} < 1$.
{{WLOG}}, assume $\norm {\dfrac a b} < 1$.
By Norm of Quotient:
:$\dfrac {\norm a} {\norm b} < 1$
Hence:
:${\norm a} < \norm b$
Let $n = \size a$ and $m = \size b$ where $\size {\,\cdot\,}$ is the absolute value on $\Q$.
Then $n, m \in \N$.
By Norm of Negative:
:$\norm n = \norm a$
:$\norm m = \norm b$
Hence:
:$\norm n < \norm m$
Since $\norm {\, \cdot \,}$ is non-Archimedean then:
:$\norm m \le 1$
Hence:
:$\norm n < \norm m \le 1$
{{qed}}
Theorem: Ostrowski's Theorem/Non-Archimedean Norm/Lemma 2.2

:$n_0$ is a prime number.

Proof:
{{AimForCont}} $n_0$ is a composite number. 
Let $n_1, n_2 \in \N$ such that $n_1, n_2 < n_0$ and $n_0 = n_1 n_2$. 
By the definition of $n_0$ then:
:$\norm {n_1} = 1$ 
:$\norm {n_2} = 1$ 
By {{NormAxiomNonArch|2}}:
:$\norm {n_0} = \norm {n_1 n_2} = \norm {n_1} \norm {n_2} = 1$
This contradicts the assumption that $\norm {n_0} < 1$. 
So $n_0$ must be a prime number.
{{qed}}
Theorem: Sum of Cosines of k pi over 5

:$\cos 36 \degrees + \cos 72 \degrees + \cos 108 \degrees + \cos 144 \degrees = 0$

Proof:
We have:
{{begin-eqn}}
{{eqn | l = 144 \degrees
      | r = 180 \degrees - 36 \degrees
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \cos 36 \degrees
      | r = -\cos 144 \degrees
      | c = Cosine of Supplementary Angle
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = 108 \degrees
      | r = 180 \degrees - 72 \degrees
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \cos 72 \degrees
      | r = -\cos 108 \degrees
      | c = Cosine of Supplementary Angle
}}
{{end-eqn}}
Thus:
:$\cos 36 \degrees + \cos 72 \degrees + \cos 108 \degrees + \cos 144 \degrees = 0$
:500px
{{qed}}
Theorem: Sum of Products of nth Roots of Unity taken up to n-1 at a Time is Zero

Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Let $U_n = \set {z \in \C: z^n = 1}$ be the complex $n$th roots of unity.
Then the sum of the products of the elements of $U_n$ taken $2, 3, 4, \dotsc n - 1$ at a time is zero.

Proof:
The elements of $U_n = \set {z \in \C: z^n = 1}$ are the solutions to the equation:
:$z^n - 1 = 0$
Thus by definition the coefficients of the powers of $z$:
:$z^2, z^3, \ldots, z^{n - 1}$
are all zero.
The result follows directly from Viète's Formulas.
{{qed}}
Theorem: Absolute Value of Complex Dot Product is Commutative

Let $z_1$ and $z_2$ be complex numbers.
Let $z_1 \circ z_2$ denote the (complex) dot product of $z_1$ and $z_2$.
Then:
:$\size {z_1 \circ z_2} = \size {z_2 \circ z_1}$
where $\size {\, \cdot \,}$ denotes the absolute value function.

Proof:
From Dot Product Operator is Commutative:
:$z_1 \circ z_2 = z_2 \circ z_1$
The result follows trivially.
{{qed}}
Theorem: Absolute Value of Complex Cross Product is Commutative

Let $z_1$ and $z_2$ be complex numbers.
Let $z_1 \times z_2$ denote the (complex) cross product of $z_1$ and $z_2$.
Then:
:$\size {z_1 \times z_2} = \size {z_2 \times z_1}$
where $\size {\, \cdot \,}$ denotes the absolute value function.

Proof:
{{begin-eqn}}
{{eqn | l = \size {z_2 \times z_1}
      | r = \size {-z_1 \times z_2}
      | c = Complex Cross Product is Anticommutative
}}
{{eqn | r = \size {z_1 \times z_2}
      | c = {{Defof|Absolute Value}}
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Area of Quadrilateral in Determinant Form

Let $A = \tuple {x_1, y_1}$, $B = \tuple {x_2, y_2}$, $C = \tuple {x_3, y_3}$ and $D = \tuple {x_4, y_4}$ be points in the Cartesian plane.
Let $A$, $B$, $C$ and $D$ form the vertices of a quadrilateral.
The area $\AA$ of $\Box ABCD$ is given by:
:<nowiki>$\AA = \dfrac 1 2 \paren {\size {\paren {\begin{vmatrix}
x_1 & y_1 & 1 \\
x_2 & y_2 & 1 \\
x_3 & y_3 & 1 \\
\end{vmatrix} } } + \size {\paren {\begin{vmatrix}
x_1 & y_1 & 1 \\
x_4 & y_4 & 1 \\
x_3 & y_3 & 1 \\
\end{vmatrix} } } }$</nowiki>

Proof:
$\Box ABCD$ can be divided into $2$ triangles: $\triangle ABC$ and $\triangle ADC$.
Hence $\AA$ is the sum of the areas of $\triangle ABC$ and $\triangle ADC$.
From Area of Triangle in Determinant Form:
{{begin-eqn}}
{{eqn | l = \map \Area {\triangle ABC}
      | r = <nowiki>\dfrac 1 2 \size {\paren {\begin{vmatrix}
x_1 & y_1 & 1 \\
x_2 & y_2 & 1 \\
x_3 & y_3 & 1 \\
\end{vmatrix} } }</nowiki>
}}
{{eqn | l = \map \Area {\triangle ADC}
      | r = <nowiki>\dfrac 1 2 \size {\paren {\begin{vmatrix}
x_1 & y_1 & 1 \\
x_4 & y_4 & 1 \\
x_3 & y_3 & 1 \\
\end{vmatrix} } }</nowiki>
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Three Points in Ultrametric Space have Two Equal Distances/Corollary 5

Let $\norm {\, \cdot \,}$ be a non-trivial non-Archimedean norm on the rational numbers $\Q$.
Let $a, b \in \Z_{\ne 0}$ be coprime:
:$a \perp b$
Then:
:$\norm a = 1$ or $\norm b = 1$

Proof:
By Bézout's Identity then:
:$\exists n, m \in \Z : m a + n b = 1$  
By Norm of Unity:
:$\norm {m a + n b} = 1$
By {{Corollary|Characterisation of Non-Archimedean Division Ring Norms|5}}:
:$\norm a, \norm b, \norm n, \norm m \le 1$
Let $\norm a < 1$.
By {{Norm-axiom-mult|2}}:
:$\norm {m a} = \norm m \norm a < 1$
Hence:
:$\norm {m a} < \norm {m a + n b}$
By {{Corollary|Three Points in Ultrametric Space have Two Equal Distances|4}}:
:$\norm {n b} = \norm {m a + n b} = 1$
By {{Norm-axiom-mult|2}}:
:$\norm n \norm b = 1$
Hence:
:$\norm b = 1$
The result follows.
{{qed}}
Theorem: Exponential of 2 m i Arccotangent of p

:$\map \exp {2 m i \arccot p} \paren {\dfrac {p i + 1} {p i - 1} }^m = 1$

Proof:
Let $z = \arccot p$.
Then:
{{begin-eqn}}
{{eqn | l = p
      | r = \frac {\cos z} {\sin z}
      | c = {{Defof|Real Arccotangent}}
}}
{{eqn | ll= \leadsto
      | l = p
      | r = i \dfrac {\map \exp {i z} + \map \exp {-i z} } {\map \exp {i z} - \map \exp {-i z} }
      | c = Euler's Cotangent Identity
}}
{{eqn | r = \frac {i \paren {\map \exp {2 i z} + 1} } {\map \exp {2 i z} - 1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = p \paren {\map \exp {2 i z} - 1}
      | r = i \paren {\map \exp {2 i z} + 1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {p - i} \map \exp {2 i z}
      | r = p + i
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \exp {2 i z}
      | r = \frac {p + i} {p - i}
      | c = 
}}
{{end-eqn}}
So we have:
{{begin-eqn}}
{{eqn | l = \map \exp {2 m i \arccot p}
      | r = \paren {\map \exp {2 i \arccot p} }^m
      | c = 
}}
{{eqn | r = \paren {\frac {p + i} {p - i} }^m
      | c = 
}}
{{end-eqn}}
Now:
{{begin-eqn}}
{{eqn | l = \paren {\frac {p + i} {p - i} } \paren {\frac {p i + 1} {p i - 1} }
      | r = \frac {p^2 i + p i^2 + p + i} {p^2 i - p i^2 - p + i}
      | c = 
}}
{{eqn | r = \frac {p^2 i + i} {p^2 i + i}
      | c = 
}}
{{eqn | r = 1
      | c = 
}}
{{end-eqn}}
and the result follows.
{{qed}}
Theorem: Modulus z - 1 Less than Modulus z + 1 iff Real z Greater than Zero

Let $z \in \C$ be a complex number.
Then:
:$\cmod {z - 1} < \cmod {z + 1} \iff \map \Re z > 0$

Proof:
{{begin-eqn}}
{{eqn | l = \cmod {z - 1}
      | o = <
      | r = \cmod {z + 1}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \cmod {z + 1}
      | o = >
      | r = \cmod {z - 1}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \paren {x + 1}^2 + y^2
      | o = >
      | r = \paren {x - 1}^2 + y^2
      | c = {{Defof|Complex Modulus}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \paren {x + 1}^2
      | o = >
      | r = \paren {x - 1}^2
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x^2 + 2 x + 1
      | o = >
      | r = x^2 - 2 x + 1
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = 4 x
      | o = >
      | r = 0
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = >
      | r = 0
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \Re z
      | o = >
      | r = 0
      | c = {{Defof|Real Part}}
}}
{{end-eqn}}
{{qed}}
Theorem: Vertices of Equilateral Triangle in Complex Plane/Sufficient Condition

Let $z_1$, $z_2$ and $z_3$ be complex numbers.
Let $z_1$, $z_2$ and $z_3$ represent on the complex plane the vertices of an equilateral triangle.
Then:
:${z_1}^2 + {z_2}^2 + {z_3}^2 = z_1 z_2 + z_2 z_3 + z_3 z_1$

Proof:
Let $T$ be the equilateral triangle whose vertices are $z_1$, $z_2$ and $z_3$.
We have that $z_2 - z_1$ and $z_3 - z_1$ are two sides of $T$ which meet at $z_1$.
From the geometry of $T$ it follows that $z_2 - z_1$ is at an angle of $\pi/3$ to $z_3 - z_1$.
Similarly, $z_1 - z_3$ and $z_2 - z_3$ are two sides of $T$ which meet at $z_3$.
From the geometry of $T$ it follows that $z_1 - z_3$ is at an angle of $\pi / 3$ to $z_2 - z_3$.
From {{Corollary|Complex Multiplication as Geometrical Transformation}}:
{{begin-eqn}}
{{eqn | n = 1
      | l = z_2 - z_1
      | r = e^{i \pi / 3} \paren {z_3 - z_1}
}}
{{eqn | n = 2
      | l = z_1 - z_3
      | r = e^{i \pi / 3} \paren {z_2 - z_3}
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \dfrac {z_2 - z_1} {z_1 - z_3}
      | r = \dfrac {z_3 - z_1} {z_2 - z_3}
      | c = $(1)$ divided by $(2)$
}}
{{eqn | ll= \leadsto
      | l = \paren {z_2 - z_1} \paren {z_2 - z_3}
      | r = \paren {z_3 - z_1} \paren {z_1 - z_3}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = {z_2}^2 - z_1 z_2 - z_2 z_3 + z_3 z_1
      | r = - {z_1}^2 - {z_3}^2 + 2 z_3 z_1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = {z_1}^2 + {z_2}^2 + {z_3}^2
      | r = z_1 z_2 + z_2 z_3 + z_3 z_1
      | c = 
}}
{{end-eqn}}
Theorem: Vertices of Equilateral Triangle in Complex Plane/Necessary Condition

Let $z_1$, $z_2$ and $z_3$ be complex numbers.
Let $z_1$, $z_2$ and $z_3$ fulfil the condition:
:${z_1}^2 + {z_2}^2 + {z_3}^2 = z_1 z_2 + z_2 z_3 + z_3 z_1$
Then $z_1$, $z_2$ and $z_3$ represent on the complex plane the vertices of an equilateral triangle.

Proof:
Let:
:${z_1}^2 + {z_2}^2 + {z_3}^2 = z_1 z_2 + z_2 z_3 + z_3 z_1$
Then:
{{begin-eqn}}
{{eqn | l = {z_1}^2 + {z_2}^2 + {z_3}^2
      | r = z_1 z_2 + z_2 z_3 + z_3 z_1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = {z_2}^2 - z_1 z_2 - z_2 z_3 + z_3 z_1
      | r = - {z_1}^2 - {z_3}^2 + 2 z_3 z_1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {z_2 - z_1} \paren {z_2 - z_3}
      | r = \paren {z_3 - z_1} \paren {z_1 - z_3}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {z_2 - z_1} {z_1 - z_3}
      | r = \dfrac {z_3 - z_1} {z_2 - z_3}
      | c = 
}}
{{end-eqn}}
Thus $z_2 - z_1$ and $z_3 - z_1$ are at the same angle to each other as $z_1 - z_3$ and $z_2 - z_1$.
Similarly:
{{begin-eqn}}
{{eqn | l = {z_1}^2 + {z_2}^2 + {z_3}^2
      | r = z_1 z_2 + z_2 z_3 + z_3 z_1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = - {z_2}^2 - {z_1}^2 + 2 z_1 z_2
      | r = {z_3}^2 - z_1 z_3 - z_2 z_3 + z_1 z_2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {z_2 - z_1} \paren {z_1 - z_2}
      | r = \paren {z_3 - z_1} \paren {z_3 - z_2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {z_2 - z_1} {z_3 - z_2}
      | r = \dfrac {z_3 - z_1} {z_1 - z_2}
      | c = 
}}
{{end-eqn}}
Thus $z_2 - z_1$ and $z_3 - z_1$ are at the same angle to each other as $z_1 - z_2$ and $z_3 - z_2$.
Thus all three angles:
:$\angle z_2 z_1 z_3$
:$\angle z_1 z_3 z_2$
:$\angle z_3 z_2 z_1$
are equal.
By definition, therefore, $\triangle z_1 z_2 z_3$ is equilateral.
Theorem: Squares of Diagonals of Parallelogram

Let $ABCD$ be a parallelogram.
:400px
Then:
:$AC^2 + BD^2 = AB^2 + BC^2 + CD^2 + DA^2$

Proof:
{{begin-eqn}}
{{eqn | l = AC^2
      | r = AB^2 + BC^2 - 2 (AB) (BC) \cos \angle B
      | c = Cosine Rule
}}
{{eqn | l = BD^2
      | r = BC^2 + CD^2 - 2 (CD) (BC) \cos \angle C
      | c = Cosine Rule
}}
{{eqn | r = DA^2 + CD^2 - 2 (AB) (CD) \cos \angle C
      | c = as $AB = CD$ and $BC = DA$
}}
{{eqn | ll= \leadsto
      | l = AC^2 + BD^2
      | r = AB^2 + BC^2 + DA^2 + CD^2 - 2 (AB) (BC) \paren {\cos \angle B + \cos \angle C}
      | c = 
}}
{{end-eqn}}
But we have that $\angle C$ and $\angle B$ are supplementary:
:$\angle C = \angle B = 180 \degrees$
Thus from Cosine of Supplementary Angle:
:$\cos \angle B + \cos \angle C = 0$
The result follows.
{{Qed}}
Theorem: Geodesic Equation/2d Surface Embedded in 3d Euclidean Space/Cylinder

Let $\sigma$ be the surface of a cylinder.
Let $\sigma$ be embedded in 3-dimensional Euclidean space.
Let $\sigma$ be parameterised by $\tuple {\phi, z}$ as
:$\mathbf r = \tuple {a \cos \phi, a \sin \phi, z}$
where
:$a > 0$
and
:$z, \phi \in \R$
Then geodesics on $\sigma$ are of the following form:
:$z = C_1 \phi + C_2$
where $C_1, C_2$ are real arbitrary constants.

Proof:
From the given parametrization it follows that:
{{begin-eqn}}
{{eqn | l = E
      | r = \mathbf r_\phi \cdot \mathbf r_\phi
}}
{{eqn | r = \tuple {-a \sin \phi, a \cos \phi, 0} \cdot \tuple {-a \sin \phi, a \cos \phi, 0}
}}
{{eqn | r = a^2
}}
{{eqn | l = F
      | r = \mathbf r_\phi \cdot \mathbf r_z
}}
{{eqn | r = \tuple {-a \sin \phi, a \cos \phi, 0} \cdot \tuple {0, 0, 1}
}}
{{eqn | r = 0
}}
{{eqn | l = G
      | r = \mathbf r_z \cdot \mathbf r_z
}}
{{eqn | r = \tuple {0, 0, 1} \cdot \tuple {0, 0, 1}
}}
{{eqn | r = 1
}}
{{end-eqn}}
where $E, F, G$ are the functions of the first fundamental form.
Furthermore, all derivatives of $E, F, G$ {{WRT|Differentiation}} $\phi$ and $z$ vanish.
Then geodesic equations read:
:$\dfrac \d {\d t} \dfrac {a^2 \phi'} {\sqrt {a^2 \phi'^2 + z'^2} } = 0$
:$\dfrac \d {\d t} \dfrac {z'} {\sqrt {a^2 \phi'^2 + z'^2} } = 0$
Integrate these differential equations once:
:$\dfrac {a^2 \phi'} {\sqrt {a^2 \phi'^2 + z'^2} } = b_1$
:$\dfrac {z'} {\sqrt {a^2 \phi'^2 + z'^2} } = b_2$
where $b_1, b_2$ are real arbitrary constants.
Divide the first equation by the second one:
:$\dfrac {a^2 \phi'} {z'} = \dfrac {b_1} {b_2}$
To solve this in terms of $z$ as a function of $\phi$, define:
:$C_1 = \dfrac {a^2 b_2} {b_1}$ 
and use the chain rule:
:$\dfrac {\d z} {\d \phi} = C_1$
Integration {{WRT|Integration}} $\phi$ yields the desired result.
In other words, geodesics are helical lines.
{{qed}}