avewright/proofwiki-math huggingface dataset:
Theorem: Binomial Distribution Approximated by Normal Distribution

Let $X$ be a discrete random variable which has the binomial distribution $\Binomial n p$.
Then for large $n$ and such that both $n p$ and $n q$ are approximately $5$ or more:
:$\Binomial n p \approx \Gaussian {n p} {n p q}$
where $\Gaussian {n p} {n p q}$ denotes the normal distribution.

Proof:
Let $Y_1, Y_2, \ldots, Y_n$ be independent random variables which have the Bernoulli Distribution $\Bernoulli p$.
By the Sum of Independent Bernoulli Random Variables is Binomial, we have that:
:$\ds \sum_{i \mathop = 1}^n Y_i \sim \Binomial n p$
{{MissingLinks|Search for theorem of Sum of Independent Bernoulli Random Variables is Binomial on ProofWiki}}
By the Central Limit Theorem, we have
:$\dfrac {\ds \sum_{i \mathop = 1}^n Y_i - n p} {\sqrt {n p q} } \xrightarrow d \Gaussian 0 1$
{{explain|meaning of $\xrightarrow d$}}
Therefore for a sufficiently large $n$:
:$\dfrac {\ds \sum_{i \mathop = 1}^n Y_i - n p} {\sqrt {n p q} } \approx \Gaussian 0 1$
Observe that:
{{begin-eqn}}
{{eqn | l = \frac {\ds \sum_{i \mathop = 1}^n Y_i - n p} {\sqrt {n p q} }
      | o = \approx
      | r = \Gaussian 0 1
}}
{{eqn | ll= \leadsto
      | l = \sum_{i \mathop = 1}^n Y_i
      | o = \approx
      | r = \Gaussian {n p} {n p q}
      | c = by Linear Transformation of Normal Random Variable with the transformation $\map f Z = \sqrt {n p q} Z + n p$
}}
{{end-eqn}}
Hence: 
:$\Binomial n p \approx \Gaussian {n p} {n p q}$
{{qed}}
Theorem: Position Vector of Midpoint of Line

Let $\mathbf a$ and $\mathbf b$ be the position vectors of points $A$ and $B$.
The position vector $\mathbf r$ of the midpoint of the line segment $AB$ is given by:
:$\mathbf r = \dfrac {\mathbf a + \mathbf b} 2$

Proof:
From Point dividing Line Segment between Two Points in Given Ratio:
:the position vector $\mathbf r$ of a point $R$ on $AB$ which divides $AB$ in the ratio $m : n$ is given by:
:$\mathbf r = \dfrac {n \mathbf a + m \mathbf b} {m + n}$
In this case the ratio $m : n$ is $1 : 1$.
Hence when $\mathbf r$ is the position vector of the midpoint of $AB$:
{{begin-eqn}}
{{eqn | l = \mathbf r
      | r = \dfrac {1 \times \mathbf a + 1 \times \mathbf b} {1 + 1}
      | c = 
}}
{{eqn | r = \dfrac {\mathbf a + \mathbf b} 2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Absolutely Convergent Generalized Sum over Union of Disjoint Index Sets

Let $V$ be a Banach space.
Let $I$ and $J$ be disjoint indexing sets.
Let $K = I \cup J$.
Let $\family{v_k}_{k \mathop \in K}$ be an indexed family of elements of $V$.
Then:
:the generalized sum $\ds \sum_{k \mathop \in K} v_k$ converges absolutely
{{iff}}
:the generalized sums $\ds \paren{\sum_{i \mathop \in I} v_i}$ and $\ds \paren{\sum_{j \mathop \in J} v_j}$ converge absolutely
In which case:
:$\ds \sum_{k \mathop \in K} \norm{v_k} = \paren{\sum_{i \mathop \in I} \norm{v_i}} + \paren{\sum_{j \mathop \in J} \norm{v_j}}$

Proof:
=== Necessary Condition ===
Let $\ds \sum_{k \mathop \in K} v_k$ converge absolutely.
By definition of absolute net convergence:
:$\ds \sum_{k \mathop \in K} \norm{v_k}$ converges.
From Generalized Sum over Subset of Absolutely Convergent Generalized Sum is Absolutely Convergent:
:$\ds \paren{\sum_{i \mathop \in I} \norm{v_i}}$ and $\ds \paren{\sum_{j \mathop \in J} \norm{v_j}}$ converge
By definition of absolute net convergence:
:$\ds \paren{\sum_{i \mathop \in I} v_i}$ and $\ds \paren{\sum_{j \mathop \in J} v_j}$ converge absolutely.
From Generalized Sum over Union of Disjoint Index Sets:
:$\ds \sum_{k \mathop \in K} \norm{v_k} = \paren{\sum_{i \mathop \in I} \norm{v_i}} + \paren{\sum_{j \mathop \in J} \norm{v_j}}$
{{qed|lemma}}
Theorem: Product of Sequentially Computable Real-Valued Functions is Sequentially Computable

Let $D \subseteq \R^n$ be a subset of real cartesian $n$-space.
Let $f, g : D \to \R$ be sequentially computable.
Then, $h : D \to \R$ defined as:
:$\map h \bsx = \map f \bsx \map g \bsx$
is sequentially computable.

Proof:
Follows immediately from:
* Real Multiplication is Sequentially Computable
* Composition of Sequentially Computable Real-Valued Functions is Sequentially Computable
{{qed}}
Category:Computability Theory
9cq5yuvkh4nb0jrwzner72b0uib2lhl
Theorem: Sum of Sequentially Computable Real-Valued Functions is Sequentially Computable

Let $D \subseteq \R^n$ be a subset of real cartesian $n$-space.
Let $f, g : D \to \R$ be sequentially computable.
Then, $h : D \to \R$ defined as:
:$\map h \bsx = \map f \bsx + \map g \bsx$
is sequentially computable.

Proof:
Follows immediately from:
* Real Addition is Sequentially Computable
* Composition of Sequentially Computable Real-Valued Functions is Sequentially Computable
{{qed}}
Category:Computability Theory
m0ylg14hcx42e8bv9sx9qjpfut2fz0x
Theorem: Constant Function of Computable Real Number is Sequentially Computable

Let $c \in \R$ be a computable real number.
Then, $f : \R^n \to \R$, defined as:
:$\map f \bsx = c$
is sequentially computable.

Proof:
For any real sequence $\sequence {x_n}$, we have:
:$\sequence {\map f {x_n}} = \sequence c$
Thus, the result follows from Constant Sequence of Computable Real Number is Computable.
{{qed}}
Category:Computability Theory
pcvt3i05a6st2kb953vcu9sm5hn97a8
Theorem: Condition for Limits of Computable Real Sequences to be Computable

Let $\sequence {x_k}_{k \in \N}$ be a computable real sequence.
Let $\sequence {y_n}_{n \in \N}$ be a real sequence.
If there exists total recursive function $\phi : \N^2 \to \N$ such that:
:$\forall n, p \in \N: \size {x_{\map \phi {n, p}} - y_n} < \dfrac 1 {p + 1}$
then:
:$\sequence {y_n}_{n \in \N}$
is a computable real sequence.

Proof:
By {{Corollary|Computable Real Sequence iff Limits of Computable Rational Sequences}}, there exists a computable rational sequence $\sequence {a_N}$ such that, for all $k, p \in \N$:
:$\size {a_{\map \pi {k, p} } - x_k} < \dfrac 1 {p + 1}$
where $\pi$ is the Cantor pairing function.
Let $\psi : \N^2 \to \N$ be defined as:
:$\map \psi {n, p} = \map \pi {\map \phi {n, 2 p + 1}, 2 p + 1}$
which is total recursive by:
* Cantor Pairing Function is Primitive Recursive
* Primitive Recursive Function is Total Recursive Function
By {{Corollary|Computable Subsequence of Computable Rational Sequence is Computable}}, there exists a computable rational sequence $\sequence {b_N}$ such that, for all $n, p \in \N$:
:$b_{\map \pi {n, p}} = a_{\map \psi {n, p}}$
We have, for all $n, p \in \N$:
{{begin-eqn}}
{{eqn | l = \size {b_{\map \pi {n, p} } - y_n}
      | r = \size {a_{\map \psi {n, p} } - y_n}
      | c = Definition of $\sequence {b_N}$
}}
{{eqn | r = \size {a_{\map \pi {\map \phi {n, 2 p + 1}, 2 p + 1} } - y_n}
      | c = Definition of $\psi$
}}
{{eqn | o = \le
      | r = \size {a_{\map \pi {\map \phi {n, 2 p + 1}, 2 p + 1} } - x_{\map \phi {n, 2 p + 1} } } + \size {x_{\map \phi {n, 2 p + 1} } - y_n}
      | c = Triangle Inequality for Real Numbers
}}
{{eqn | o = <
      | r = \dfrac 1 {2 p + 2} + \dfrac 1 {2 p + 2}
      | c = Premise
}}
{{eqn | r = \dfrac 1 {p + 1}
}}
{{end-eqn}}
The result then follows from {{Corollary|Computable Real Sequence iff Limits of Computable Rational Sequences}}.
{{qed}}
Category:Computability Theory
27hcwh880lgm7jd9u4o7yi7ytviexl7
Theorem: L1 Mean Ergodic Theorem

Let $\struct {X, \BB, \mu, T}$ be a measure-preserving dynamical system.
Let $\map {L^1_\C} \mu$ be the complex-valued $L^1$ space of $\mu$.
Then for each $f \in \map {L^1_\C} \mu$ there is a $T$-invariant function $\tilde f \in \map {L^1_\C} \mu$ such that:
:$\ds \lim_{N \mathop \to \infty} \dfrac 1 N \sum_{n \mathop = 0}^{N - 1} f \circ T^n = \tilde f$ converges in the $L^1$-norm

Proof:
For $c > 0$ let:
:$f_c = f \cdot \chi_{\set {\cmod f \mathop \le c} }$
where $\chi_B$ is the characteristic function of $B$.
By Lebesgue's Dominated Convergence Theorem:
{{begin-eqn}}
{{eqn | l = f - f_c
      | r = f \cdot \paren {1 -\chi_{\set {\cmod f \mathop \le c} } }
}}
{{eqn | r = f \cdot \chi_{\set {\cmod f \mathop > c} }
}}
{{eqn | o = \to
      | r = 0
      | c = in $\map {L^1_\C} \mu$ as $c \to +\infty$
}}
{{end-eqn}}
{{qed|lemma}}
Let $\epsilon > 0$ be arbitrary.
Let $c > 0$ be such that:
:$\norm {f - f_c}_1 \le \dfrac \epsilon 3$
As $f_c \in \map {L^2_\C} \mu$, we can apply Mean Ergodic Theorem.
Thus by Convergent Sequence is Cauchy Sequence, there exists an $N_0 \in \N_{>0}$ such that:
:$\ds \forall M, N \ge N_0 : \norm {\dfrac 1 M \sum_{n \mathop = 0}^{M - 1} f_c \circ T^n - \dfrac 1 N \sum_{n \mathop = 0}^{N - 1} f_c \circ T^n}_1 \le \frac \epsilon 3$
in view of Schwarz's Inequality $\norm \cdot_1 \le \norm \cdot_2^2$.
Thus by {{NormAxiomVector|3}}, we obtain:
:$\ds \forall M, N \ge N_0 : \norm {\dfrac 1 M \sum_{n \mathop = 0}^{M - 1} f \circ T^n - \dfrac 1 N \sum_{n \mathop = 0}^{N - 1} f \circ T^n}_1 \le \epsilon$
That is:
:$\ds \sequence { \frac 1 N \sum_{n \mathop = 0}^{N - 1} f \circ T^n  }_N$
is a Cauchy sequence in $\map {L^1_\C} \mu$.
{{qed|lemma}}
By Riesz-Fischer Theorem there exists an $\tilde f \in \map {L^1_\C} \mu$ such that:
:$\ds \lim_{N \mathop \to \infty} \norm { \dfrac 1 N \sum_{n \mathop = 0}^{N - 1} f \circ T^n - \tilde f}_1 = 0$
Furthermore:
{{begin-eqn}}
{{eqn | l = \norm {\tilde f \circ T - \tilde f}_1
      | r = \lim_{N \mathop \to \infty} \norm {\dfrac 1 N \sum_{n \mathop = 0}^{N - 1} f \circ T^{n + 1} - \dfrac 1 N \sum_{n \mathop = 0}^{N - 1} f \circ T^n}_1
}}
{{eqn | r = \lim_{N \mathop \to \infty} \norm {\dfrac {f \circ T^N - f} N}_1
}}
{{eqn | o = \le
      | r = \lim_{N \mathop \to \infty} \dfrac {\norm {f \circ T^N}_1 + \norm f_1} N
}}
{{eqn | r = \lim_{N \mathop \to \infty} \dfrac {2 \norm f_1} N
}}
{{eqn | r = 0
}}
{{end-eqn}}
That is:
:$\tilde f \circ T = \tilde f$
{{qed}}
Theorem: Topological Space Separated by Mappings is Hausdorff

Let $X$ be a topological space.
Let $\family {Y_i}_{i \mathop \in I}$ be an indexed family of Hausdorff spaces for some indexing set $I$.
Let $\family {f_i : X \to Y_i}_{i \mathop \in I}$ be an indexed family of continuous mappings.
Suppose $\family {f_i : X \to Y_i}_{i \mathop \in I}$ separates the points of $X$.
Then, $X$ is Hausdorff.

Proof:
Let $x \ne y$ be elements of $X$.
By definition of separating points, there exists some $i \in I$ such that:
:$\map {f_i} x \ne \map {f_i} y$
As $Y_i$ is Hausdorff, there exist open sets $U, V \subseteq Y_i$ such that:
:$\map {f_i} x \in U$
:$\map {f_i} y \in V$
:$U \cap V = \O$
By definition of continuous mapping, we have that:
:$f_i^{-1} \sqbrk U$ and $f_i^{-1} \sqbrk V$ are open sets of $X$
By the definition of preimage, it is immediate that:
:$x \in f_i^{-1} \sqbrk U$
:$y \in f_i^{-1} \sqbrk V$
It remains to show that $f_i^{-1} \sqbrk U$ and $f_i^{-1} \sqbrk V$ are disjoint.
{{AimForCont}} there is some $z \in X$ such that:
:$z \in f_i^{-1} \sqbrk U$
:$z \in f_i^{-1} \sqbrk V$
Then, by definition of preimage:
:$\map {f_i} z \in U$
:$\map {f_i} z \in V$
contradicting the fact that $U$ and $V$ are themselves disjoint.
By Proof by Contradiction, it follows that $f_i^{-1} \sqbrk U$ and $f_i^{-1} \sqbrk V$ are disjoint.
As $x \ne y$ were arbitrary, it follows that $X$ is Hausdorff by definition.
{{qed}}
Category:Hausdorff Spaces
rwiw8d34ygg1gduqkxs3kafaop8hvhq
Theorem: Boundary of Compact Convex Set with Nonempty Interior is Homeomorphic to Sphere

Let $n \in \N_{> 0}$.
Let $C \subseteq \R^n$ be a compact convex subset of real Euclidean $n$-space.
Suppose that the interior $C^\circ$ is non-empty.
Then, the boundary $\partial C$ is homeomorphic to $\Bbb S^{n - 1}$, the unit $n - 1$-sphere.

Proof:
Let $\bsx_0 \in C^\circ$ be an element of $C^\circ$.
Define $\phi : \R^n \setminus \set {\bsx_0} \to \Bbb S^{n - 1}$ as:
:$\map \phi \bsx = \dfrac 1 {\norm {\bsx - \bsx_0}} \paren {\bsx - \bsx_0}$
As Normed Vector Space is Hausdorff Topological Vector Space, it follows that $\phi$ is continuous.
Define $\phi^* : \partial C \to \Bbb S^{n - 1}$ as:
:$\map {\phi^*} \bsx = \map \phi \bsx$
which is well-defined as the boundary is disjoint from the interior by definition.
By Restriction of Continuous Mapping is Continuous:
:$\phi^*$ is continuous.
{{qed|lemma}}
It remains to show that $\phi^*$ is a bijection.
Let $\bsy \in \Bbb S^{n - 1}$ be arbitrary.
We need to prove that there is a unique $\bsx \in \partial C$ such that:
:$\map \phi \bsx = \bsy$
By Ray from Interior of Compact Convex Set Meets Boundary Exactly Once, there is a unique $t \in \R_{> 0}$ such that:
:$\bsx_0 + t \bsy \in \partial C$
Therefore:
{{begin-eqn}}
{{eqn | l = \map \phi {\bsx_0 + t \bsy}
      | r = \frac 1 {\norm {t \bsy} } \paren {t \bsy}
      | c = Definition of $\phi$
}}
{{eqn | r = \bsy
      | c = {{Defof|Unit Sphere (Topology)|Unit Sphere}}
}}
{{end-eqn}}
Now, $\bsx \in \partial C$ satisfies:
:$\map \phi \bsx = \bsy$.
Then:
{{begin-eqn}}
{{eqn | l = \bsy
      | r = \map \phi \bsx
}}
{{eqn | r = \frac 1 {\norm {\bsx - \bsx_0} } \paren {\bsx - \bsx_0}
}}
{{eqn | ll = \leadsto
      | l = \norm {\bsx - \bsx_0} \bsy
      | r = \bsx - \bsx_0
}}
{{eqn | ll = \leadsto
      | l = \bsx
      | r = \bsx_0 + \norm {\bsx - \bsx_0} \bsy
}}
{{end-eqn}}
Therefore:
:$\bsx_0 + \norm {\bsx - \bsx_0} \bsy \in \partial C$
so:
:$\norm {\bsx - \bsx_0} = t$
Hence:
:$\bsx = \bsx_0 + t \bsy$
Therefore, for every $\bsy \in \Bbb S^{n - 1}$, there is a unique $\bsx \in \partial C$ such that:
:$\map {\phi^*} \bsx = \map \phi \bsx = \bsy$
and so $\phi^*$ is a bijection by definition.
{{qed|lemma}}
We have shown that $\phi^*$ is a continuous bijection.
By Boundary of Compact Set in Hausdorff Space is Compact, $\partial C$ is compact.
Therefore, by Continuous Bijection from Compact to Hausdorff is Homeomorphism:
:$\phi^*$ is a homeomorphism from $\partial C$ to $\Bbb S^{n - 1}$
{{qed}}
Category:Homeomorphisms (Topological Spaces)
sr0jxvu8nqelx4x1pceflh576a7yohm
Theorem: Similarity Dimension of Cantor Set

The Cantor set is a fractal with similarity dimension of $\dfrac {\ln 2} {\ln 3}$, which is $0 \cdotp 63$ to $2$ decimal places.

Proof:
Let $C$ denote the Cantor set.
$C$ has the following self-similarities:
{{begin-eqn}}
{{eqn | l = x
      | o = \mapsto
      | r = \dfrac x 3
      | c = with scale factor $r_1 = \dfrac 1 3$
}}
{{eqn | l = x
      | o = \mapsto
      | r = \dfrac 2 3 + \dfrac x 3
      | c = with scale factor $r_2 = \dfrac 1 3$
}}
{{end-eqn}}
Thus we have:
{{begin-eqn}}
{{eqn | l = r_1 = r_2
      | r = \dfrac 1 3
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {\dfrac 1 3}^D + \paren {\dfrac 1 3}^D
      | r = 1
      | c = {{Defof|Similarity Dimension}}: $\paren {r_1}^D + \paren {r_2}^D = 1$
}}
{{eqn | ll= \leadsto
      | l = \paren {\dfrac 1 3}^D
      | r = \dfrac 1 2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = D \ln \dfrac 1 3
      | r = \ln \dfrac 1 2
      | c = taking logs of both sides
}}
{{eqn | ll= \leadsto
      | l = D
      | r = \dfrac {\ln 2} {\ln 3}
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Chord Length for Regular Polygon

Let $P$ be a regular polygon of $n$ sides.
Let $P$ be inscribed into a circumcircle with radius $r$.
:400px
Let $CF$ be a chord of $P$, also a chord of the circumcircle.
$CF$ divides $P$ into two polygons containing $k$ and $n - k$ sides of $P$.
The length of the chord is $2 r \map \sin {\dfrac {k \pi} n}$.
{{improve|Instead of talking about circumscribed circles, can we just refer to the long radius? It might streamline a lot of the argument.}}

Proof:
Let $\theta = \angle BAC$ be an inscribed angle, subtending one of the sides of $P$, with its vertex coinciding in one of the other vertices of $P$.
Because $P$ is a regular $n$-gon, its sides are all the same length.
We have {{hypothesis}} that $P$ is inscribed into a circle.
Therefore, the central angles subtending a single side all have the same angular measure: $\dfrac {2 \pi} n$.
By the Inscribed Angle Theorem, the angles formed at the vertices of $P$ subtending a single side all have equal angular measure.
That is:
:$\theta = \dfrac \pi n$
Let $\angle CAF = \phi$ be an inscribed angle subtending the chord $CF$.
By addition:
:$\angle CAF = \angle CAD + \angle DAE + \angle EAF$
Thus, the angle $\phi$ is the sum of $k$ smaller angles each with measure $\theta$.
Hence:
:$\phi = k \theta = \dfrac {k \pi} n$
By Length of Chord of Circle:
:$CF = 2 r \map \sin {\dfrac {k \pi} n}$
{{qed}}
Theorem: Complement of Bounded Set has Exactly One Unbounded Component

Let $n \in \N_{> 1}$
Let $A \subseteq \R^n$ be a bounded subspace of real Euclidean $n$-space.
Then, $\R^n \setminus A$ has exactly one unbounded component.

Proof:
By definition of bounded, there exists some $\bsx_0 \in \R^n$ and $\epsilon > 0$ such that:
:$A \subseteq \map {B_\epsilon} {\bsx_0}$
Theorem: Convex Cone is Convex Set

Let $\GF \in \set {\R, \C}$.
Let $X$ be a vector space over $\GF$.
Let $P \subseteq X$ be a convex cone in $X$.
Then $P$ is convex.

Proof:
Let $x, y \in P$. 
Let $t \in \closedint 0 1$ so that:
:$t \ge 0$ and $1 - t \ge 0$.
Since $P$ is a cone, we have:
:$t x \in P$ and $\paren {1 - t} y \in P$.
Since $P$ is a convex cone, we have:
:$t x + \paren {1 - t} y \in P$
So $P$ is convex.
{{qed}}
Theorem: Characterization of Preordered Vector Spaces

Let $\GF \in \set {\R, \C}$.
Let $X$ be a vector space over $\GF$.
Let $\succeq$ be a preordering on $X$.
Then $\struct {X, \succeq}$ is a preordered vector space {{iff}} there exists a convex cone $P \subseteq X$ such that $\succeq$ is the preordering on $X$ induced by $P$.

Proof:
=== Necessary Condition ===
Suppose that $\struct {X, \succeq}$ is a preordered vector space.
Let:
:$P = \set {x \in X : x \succeq 0}$
Let $\succeq^P$ be the preordering on $X$ induced by $P$.
We want to show that, for $x, y \in X$, we have $x \succeq y$ {{iff}} $x \succeq^P y$.
Let $x, y \in X$.
By the definition of the preordering on $X$ induced by $P$, we have:
:$x \succeq^P y$ {{iff}} $x - y \in P$
By the definition of $P$:
:$x - y \in P$ {{iff}} $x - y \succeq 0$
Since $\struct {X, \succeq}$ is a preordered vector space, we obtain:
:$x - y \succeq 0$ {{iff}} $x \succeq y$
Hence $\succeq$ is the preordering on $X$ induced by $P$.
{{qed|lemma}}
Theorem: Lagrange's Trigonometric Identities/Sine/Cosine Form

:$\ds \sum_{k \mathop = 0}^n \sin k \theta = \dfrac {\map \cos {\frac 1 2 \theta} - \map \cos {n \theta + \frac 1 2 \theta} } {2 \map \sin {\frac 1 2 \theta} }$

Proof:
{{begin-eqn}}
{{eqn | l = \map \sin {\alpha} \map \sin {\beta}
      | r = \dfrac {\map \cos {\alpha - \beta} - \map \cos {\alpha + \beta} } 2
      | c = Werner Formula for Sine by Sine
}}
{{eqn | l = 2 \map \sin {\beta} \map \sin {\alpha}
      | r = \map \cos {\alpha - \beta} - \map \cos {\alpha + \beta}
      | c = rearranging
}}
{{eqn | l = 2 \map \sin {\frac 1 2 \theta} \cdot \map \sin {k \theta}
      | r = \map \cos {k \theta - \frac 1 2 \theta} - \map \cos {k \theta + \frac 1 2 \theta}
      | c = setting $\alpha = k \theta$ and $\beta = \frac 1 2 \theta$
}}
{{eqn | l = 2 \map \sin {\frac 1 2 \theta} \cdot  \sum_{k \mathop = 0}^n \map \sin {k \theta}
      | r = \sum_{k \mathop = 0}^n \map \cos {k \theta - \frac 1 2 \theta} - \map \cos {k \theta + \frac 1 2 \theta}
      | c = Summing both sides
}}
{{end-eqn}}
The {{RHS}} is a telescoping sum. 
{{begin-eqn}}
{{eqn | l = 2 \map \sin {\frac 1 2 \theta} \cdot  \sum_{k \mathop = 0}^n \map \sin {k \theta}
      | r = \map \cos {\frac {-1} 2 \theta} - \map \cos {n \theta + \frac 1 2 \theta}
      | c = only two terms survive
}}
{{eqn | l = 2 \map \sin {\frac 1 2 \theta} \cdot  \sum_{k \mathop = 0}^n \map \sin {k \theta}
      | r = \map \cos {\frac 1 2 \theta} - \map \cos {n \theta + \frac 1 2 \theta}
      | c = Cosine Function is Even
}}
{{eqn | l = \sum_{k \mathop = 0}^n \map \sin {k \theta}
      | r = \frac {\map \cos {\frac 1 2 \theta} - \map \cos {n \theta + \frac 1 2 \theta} }{ 2 \map \sin {\frac 1 2 \theta} }
      | c = rearranging
}}
{{end-eqn}}
{{qed}}
Theorem: Product of nth Roots of Unity

Let $n \in \Z$ be an integer such that $n > 0$.
Let $z \in \C$ be a complex number such that $z^n = 1$.
Then:
:$U_n = \set {e^{2 i k \pi / n}: k \in \N_n}$
where $U_n$ is the set of $n$th roots of unity.
That is:
:$z \in \set {1, e^{2 i \pi / n}, e^{4 i \pi / n}, \ldots, e^{2 \paren {n - 1} i \pi / n} }$
Then the product of all of the elements of $U_n$ is $(-1)^{n-1}$

Proof:
{{begin-eqn}}
{{eqn | l = \prod_{k \mathop = 0}^{n - 1} e^{2 i k \pi / n}
      | r = e^{2 i \paren {0} \pi / n} e^{2 i \paren {1} \pi / n} e^{2 i \paren {2} \pi / n} \dotsm e^{2 i \paren {n - 1} \pi / n}
      | c = 
}}
{{eqn | r = e^{\paren {2 i \pi / n} \paren {0 + 1 + \dotsm + \paren {n - 1} } }
      | c = Product of Powers
}}
{{eqn | r = e^{\paren {2 i \pi / n} \paren {\frac {n \paren {n - 1} } 2 } }
      | c = Closed Form for Triangular Numbers
}}
{{eqn | r = e^{\paren {i \pi } \paren {n - 1 } }
      | c = 
}}
{{eqn | r = \paren {-1}^{\paren {n - 1 } }
      | c = $e^{i \pi} = -1$
}}
{{end-eqn}}
{{qed}}
Category:Complex Roots of Unity
i3aoryl8thbonl3p72qntn1klziug40
Theorem: Equiangular Right Triangles are Similar

Equiangular right triangles are similar.

Proof:
This is an instance of the theorem Equiangular Triangles are Similar.
{{qed}}
Theorem: Equiangular Right Triangles are Similar

Equiangular right triangles are similar.

Proof:
Let $ABC$ be an arbitrary right triangle with $\angle ABC$ a right angle.
Construct a straight line from $A$ parallel to $BC$.
{{:Euclid:Proposition/I/31}}
Construct a second straight line from $C$ parallel to $AB$, meeting the first straight line at $D$.
By Quadrilateral is Parallelogram iff Both Pairs of Opposite Sides are Equal or Parallel:
:$\Box ABCD$ is a parallelogram.
By definition of rectangle, and from Rectangle is Parallelogram:
:$\Box ABCD$ is a rectangle.
By construction, $AC$ is a diameter of $\Box ABCD$.
:500px
Let $H$ be an arbitrary point on $AC$.
Constuct $EHF$ parallel to $BC$ intersecting $AB$ at $F$ and $CD$ at $H$.
Constuct $DGI$ parallel to $AB$ intersecting $AD$ at $G$ and $BC$ at $I$.
Hence by construction $EHF$ and $DGI$ are both parallel to the sides of $\Box ABCD$.
By Triangle Side-Side-Side Congruence:
:$\triangle ABC \cong \triangle ADC$
so:
:$\angle BAC = \angle DCA$
:$\angle DAC = \angle ACB$
By Parallelism implies Equal Corresponding Angles:
:$\angle AHF = \angle ACB$
Because the diameter of each is shared, by Triangle Angle-Side-Angle Congruence:
:$\triangle AFH \cong \triangle AGH$
:$\triangle HIC \cong \triangle HEC$
For the same reasons and also by construction:  
:$\triangle ABC \cong \triangle ADC$
By definition of congruence, $\Box ABCD$ is composed of two parts of equal area:
:$\map \AA {\triangle AFH} + \map \AA {\Box FBIH} + \map \AA {\triangle HIC}$
:$\map \AA {\triangle AGH} + \map \AA {\Box GHED} + \map \AA {\triangle HEC}$
By subtraction, we obtain:
:$\map \AA {\Box FBIH} = \map \AA {\Box GHED}$
From Area of Rectangle:
:$FH \cdot HI = GH \cdot HE$
Rearranging:
:$\dfrac {FH} {GH} = \dfrac {HE} {HI}$
Thus, corresponding sides within each right triangle have equal ratios.
and also corresponding sides compared between two right triangle have equal ratios:
:$\dfrac {FH} {HE} = \dfrac {GH} {HI}$
We can extend this result to the hypotenuse:
400px
In the above diagram, the altitude of $\triangle ABC$ is $CD$.
By Perpendicular in Right-Angled Triangle makes two Similar Triangles:
:$\triangle ADC \sim \triangle CDB$
By what we have shown above:
:$\dfrac {AC} {BC} = \dfrac {AD} {CD} = \dfrac {CD} {BD}$
Rearranging:
:$\dfrac {BC} {CD} = \dfrac {AC} {AD}$
which yields the result.
{{qed}}