avewright/proofwiki-math huggingface dataset:
Theorem: There Exists No Universal Set

There exists no set which is an absolutely universal set.
That is:
:$\map \neg {\exists \, \UU: \forall T: T \in \UU}$
where $T$ is any arbitrary object at all.
That is, a set that contains ''everything'' cannot exist.

Proof:
{{AimForCont}} such a $\UU$ exists.
Using the Axiom of Specification, we can create the set of all ordinals:
:$\set {x \in \UU: x \text{ is an ordinal} }$
But from Burali-Forti Paradox, this set cannot exist, which is a contradiction.
{{qed}}
Theorem: Union of Disjoint Singletons is Doubleton

Let $\set a$ and $\set b$ be singletons such that $a \ne b$.
Then:
:$\set a \cup \set b = \set {a, b}$

Proof:
Let $x \in \set a \cup \set b$.
Then by the Axiom of Unions:
:$x = a \lor x = b$
It follows from the Axiom of Pairing that:
:$x \in \set {a, b}$
Thus by definition of subset:
:$\set a \cup \set b \subseteq \set {a, b}$
{{qed|lemma}}
Let $x \in \set {a, b}$.
Then by the Axiom of Pairing:
:$x = a \lor x = b$
So by the Axiom of Unions:
:$x \in \set a \cup \set b$
Thus by definition of subset:
:$\set {a, b} \subseteq \set a \cup \set b$
{{qed|lemma}}
The result follows by definition of set equality.
{{qed}}
Theorem: Union of Disjoint Singletons is Doubleton

Let $\set a$ and $\set b$ be singletons such that $a \ne b$.
Then:
:$\set a \cup \set b = \set {a, b}$

Proof:
Straightforward from Union of Unordered Tuples.
{{qed}}
Theorem: Heine-Borel Theorem/Real Line/Closed and Bounded Set

Let $F$ be a closed and bounded real set.
Let $C$ be a set of open real sets.
Let $C$ be a cover of $F$.
Then there is a finite subset of $C$ that covers $F$.

Proof:
We are given that $C$ is a set of open real sets that covers $F$.
In other words, $C$ is an open cover of $F$.
We need to show that there is a finite subset of $C$ that covers $F$.
In other words, we need to show that $C$ has a finite subcover.
Let $F_o$ be the complement of $F$ in $\R$.
By definition of closed real set, $F_o$ is open as $F$ is closed.
Theorem: Cardinality of Set of All Mappings from Empty Set

Let $T$ be a set.
Let $T^\O$ denote the set of all mappings from $\O$ to $S$.
Then:
:$\card {T^\O} = 1$
where $\card {T^\O}$ denotes the cardinality of $\O^S$.

Proof:
The only element of $T^\O$ is the null relation:
:$\O \times T$
From Null Relation is Mapping iff Domain is Empty Set, $\O \times T$ is a mapping from $\O$ to $T$.
The result follows from Empty Mapping is Unique.
That is:
:$\card {T^\O} = 1$
{{qed}}
Theorem: Cardinality of Set of All Mappings to Empty Set

Let $S$ be a set.
Let $\O^S$ be the set of all mappings from $S$ to $\O$.
Then:
:$\card {\O^S} = \begin{cases}
1 & : S = \O \\ 
0 & : S \ne \O
\end{cases}$
where $\card {\O^S}$ denotes the cardinality of $\O^S$.

Proof:
From Null Relation is Mapping iff Domain is Empty Set, the null relation:
:$\RR = \O \subseteq S \times T$
is not a mapping unless $S = \O$.
So if $S \ne \O$:
:$\card {\O^S} = 0$
If $S = \O$:
:$\card {\O^S} = 1$
Hence the result.
{{qed}}
Theorem: Intersection Distributes over Union/Family of Sets/Corollary

Let $I$ and $J$ be indexing sets.
Let $\family {A_\alpha}_{\alpha \mathop \in I}$ and $\family {B_\beta}_{\beta \mathop \in J}$ be indexed families of subsets of a set $S$.
Then:
:$\ds \bigcup_{\tuple {\alpha, \beta} \mathop \in I \times J} \paren {A_\alpha \cap B_\beta} = \paren {\bigcup_{\alpha \mathop \in I} A_\alpha} \cap \paren {\bigcup_{\beta \mathop \in J} B_\beta}$
where $\ds \bigcup_{\alpha \mathop \in I} A_\alpha$ denotes the union of $\family {A_\alpha}_{\alpha \mathop \in I}$.

Proof:
{{begin-eqn}}
{{eqn | l = \bigcup_{\alpha \mathop \in I} \paren {A_\alpha \cap B}
      | r = \paren {\bigcup_{\alpha \mathop \in I} A_\alpha} \cap B
      | c = Intersection Distributes over Union of Family
}}
{{eqn | ll= \leadsto
      | l = \bigcup_{\alpha \mathop \in I} \paren {A_\alpha \cap \paren {\bigcup_{\beta \mathop \in J} B_\beta} }
      | r = \paren {\bigcup_{\alpha \mathop \in I} A_\alpha} \cap \paren {\bigcup_{\beta \mathop \in J} B_\beta}
      | c = setting $\ds B = \paren {\bigcup_{\beta \mathop \in J} B_\beta}$
}}
{{eqn | ll= \leadsto
      | l = \bigcup_{\alpha \mathop \in I} \paren {\bigcup_{\beta \mathop \in J} \paren {A_\alpha \cap B_\beta} }
      | r = \paren {\bigcup_{\alpha \mathop \in I} A_\alpha} \cap \paren {\bigcup_{\beta \mathop \in J} B_\beta}
      | c = Intersection Distributes over Union of Family
}}
{{eqn | ll= \leadsto
      | l = \bigcup_{\paren {\alpha, \beta} \mathop \in I \times J} \paren {A_\alpha \cap B_\beta}
      | r = \paren {\bigcup_{\alpha \mathop \in I} A_\alpha} \cap \paren {\bigcup_{\beta \mathop \in J} B_\beta}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Union Distributes over Intersection/Family of Sets/Corollary

Let $I$ and $J$ be indexing sets.
Let $\family {A_\alpha}_{\alpha \mathop \in I}$ and $\family {B_\beta}_{\beta \mathop \in J}$ be indexed families of subsets of a set $S$.
Then:
:$\ds \bigcap_{\tuple{\alpha, \beta} \mathop \in I \times J} \paren {A_\alpha \cup B_\beta} = \paren {\bigcap_{\alpha \mathop \in I} A_\alpha} \cup \paren {\bigcap_{\beta \mathop \in J} B_\beta}$
where $\ds \bigcap_{\alpha \mathop \in I} A_\alpha$ denotes the intersection of $\family {A_\alpha}_{\alpha \mathop \in I}$.

Proof:
{{begin-eqn}}
{{eqn | l = \bigcap_{\alpha \mathop \in I} \paren {A_\alpha \cup B}
      | r = \paren {\bigcap_{\alpha \mathop \in I} A_\alpha} \cup B
      | c = Union Distributes over Intersection of Family
}}
{{eqn | ll= \leadsto
      | l = \bigcap_{\alpha \mathop \in I} \paren {A_\alpha \cup \paren {\bigcap_{\beta \mathop \in J} B_\beta} }
      | r = \paren {\bigcap_{\alpha \mathop \in I} A_\alpha} \cup \paren {\bigcap_{\beta \mathop \in J} B_\beta}
      | c = setting $\ds B = \paren {\bigcap_{\beta \mathop \in J} B_\beta}$
}}
{{eqn | ll= \leadsto
      | l = \bigcap_{\alpha \mathop \in I} \paren {\bigcap_{\beta \mathop \in J} \paren {A_\alpha \cup B_\beta} }
      | r = \paren {\bigcap_{\alpha \mathop \in I} A_\alpha} \cup \paren {\bigcap_{\beta \mathop \in J} B_\beta}
      | c = Union Distributes over Intersection of Family
}}
{{eqn | ll= \leadsto
      | l = \bigcap_{\paren {\alpha, \beta} \mathop \in I \times J} \paren {A_\alpha \cup B_\beta}
      | r = \paren {\bigcap_{\alpha \mathop \in I} A_\alpha} \cup \paren {\bigcap_{\beta \mathop \in J} B_\beta}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Cartesian Product of Unions/General Result

Let $I$ and $J$ be indexing sets.
Let $\family {A_i}_{i \mathop \in I}$ and $\family {B_j}_{j \mathop \in J}$ be families of sets indexed by $I$ and $J$ respectively.
Then:
:$\ds \paren {\bigcup_{i \mathop \in I} A_i} \times \paren {\bigcup_{j \mathop \in J} B_j} = \bigcup_{\tuple {i, j} \mathop \in I \times J} \paren {A_i \times B_j}$
where:
:$\ds \bigcup_{i \mathop \in I} A_i$ denotes the union of $\family {A_i}_{i \mathop \in I}$ and so on
:$\times$ denotes Cartesian product.

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = \tuple {x, y} \in \paren {\bigcup_{i \mathop \in I} A_i} \times \paren {\bigcup_{j \mathop \in J} B_j}
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | r = \paren {\exists i \in I: x \in A_i}
}}
{{eqn | o = \land
      | r = \paren {\exists j \in J: y \in B_j}
      | c = {{Defof|Cartesian Product}} and {{Defof|Set Union}}
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | r = \exists i \in I \exists j \in J: \paren {x \in A_i} \land \paren {y \in B_j}
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | r = \exists \tuple {i, j} \in I \times J: \tuple {x, y} \in A_i \times B_j
      | c = {{Defof|Cartesian Product}}
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | r = \tuple {x, y} \in \bigcup_{\tuple {i, j} \mathop \in I \times J} \paren {A_i \times B_j}
      | c = {{Defof|Set Union}}
}}
{{end-eqn}}
{{qed}}
Theorem: Preimages All Exist iff Surjection/Corollary

:$\forall B \subseteq T, B \ne \O: f^{-1} \sqbrk B \ne \O$
{{iff}}:
:$f$ is a surjection
where $f^{-1} \sqbrk B$ denotes the preimage of $B \subseteq T$.

Proof:
=== Necessary Condition ===
Let $f$ be a surjection.
Let $B \subseteq T$ such that $B \ne \O$.
Then:
:$\exists t \in T: t \in B$
From Preimages All Exist iff Surjection:
:$\map {f^{-1} } t \ne \O$
As $t \in B$ it follows from Preimage of Subset is Subset of Preimage that:
:$f^{-1} \sqbrk B \ne \O$
$B$ is arbitrary, so:
:$\forall B \subseteq T, B \ne \O: f^{-1} \sqbrk B \ne \O$
{{qed|lemma}}
Theorem: Image of Preimage under Relation is Subset

Let $\RR \subseteq S \times T$ be a relation.
Then:
:$B \subseteq T \implies \paren {\RR \circ \RR^{-1} } \sqbrk B \subseteq B$
where:
:$\RR \sqbrk B$ denotes the image of $B$ under $\RR$
:$\RR^{-1} \sqbrk B$ denotes the preimage of $B$ under $\RR$
:$\RR \circ \RR^{-1}$ denotes composition of $\RR$ and $\RR^{-1}$.

Proof:
Let $B \subseteq T$.
Then:
{{begin-eqn}}
{{eqn | l = y
      | o = \in
      | r = \paren {\RR \circ \RR^{-1} } \sqbrk B
}}
{{eqn | ll= \leadsto
      | l = y
      | o = \in
      | r = \RR \sqbrk {\RR^{-1} \sqbrk B}
      | c = {{Defof|Composition of Relations}}
}}
{{eqn | ll= \leadsto
      | q = \exists x \in \RR^{-1} \sqbrk B
      | l = \tuple {x, y}
      | o = \in
      | r = \RR
}}
{{eqn | ll= \leadsto
      | l = y
      | o = \in
      | r = B
      | c =
}}
{{end-eqn}}
So by definition of subset:
:$B \subseteq T \implies \paren {\RR \circ \RR^{-1} }\sqbrk B \subseteq B$
{{qed}}
Theorem: Inverse of Direct Image Mapping does not necessarily equal Inverse Image Mapping

Let $S$ and $T$ be sets.
Let $\RR \subseteq S \times T$ be a relation.
Let $\RR^\to$ be the direct image mapping of $\RR$.
Let $\RR^\gets$ be the inverse image mapping of $\RR$.
Then it is not necessarily the case that:
:$\paren {\RR^\to}^{-1} = \RR^\gets$
where $\paren {\RR^\to}^{-1}$ denote the inverse of $\RR^\to$.
That is, the inverse of the direct image mapping of $\RR$ does not always equal the inverse image mapping of $\RR$.

Proof:
Proof by Counterexample:
Let $S = T = \set {0, 1}$.
Let $\RR = \set {\tuple {0, 0}, \tuple {0, 1} }$.
We have that:
:$\RR^{-1} = \set {\tuple {0, 0}, \tuple {1, 0} }$
:$\powerset S = \powerset T = \set {\O, \set 0, \set 1, \set {0, 1} }$
Thus, by inspection:
{{begin-eqn}}
{{eqn | l = \map {\RR^\to} \O
      | r = \O
      | c = 
}}
{{eqn | l = \map {\RR^\to} {\set 0}
      | r = \set {0, 1}
      | c = 
}}
{{eqn | l = \map {\RR^\to} {\set 1}
      | r = \O
      | c = 
}}
{{eqn | l = \map {\RR^\to} {\set {0, 1} }
      | r = \set {0, 1}
      | c = 
}}
{{end-eqn}}
Note that $\paren {\RR^\to}^{-1}$ is the inverse of a mapping which is neither an injection nor a surjection, and so is itself not a mapping from $\powerset T$ to $\powerset S$.
{{begin-eqn}}
{{eqn | l = \map {\paren {\RR^\to}^{-1} } \O
      | r = \set {\O, \set 1}
      | c = 
}}
{{eqn | l = \map {\paren {\RR^\to}^{-1} } {\set 0}
      | r = \O
      | c = 
}}
{{eqn | l = \map {\paren {\RR^\to}^{-1} } {\set 1}
      | r = \O
      | c = 
}}
{{eqn | l = \map {\paren {\RR^\to}^{-1} } {\set {0, 1} }
      | r = \set {\set 0, \set {0, 1} }
      | c = 
}}
{{end-eqn}}
This can be seen to be completely different from $\RR^\gets$, which can be determined by inspection to be:
{{begin-eqn}}
{{eqn | l = \map {\RR^\gets} \O
      | r = \O
      | c = 
}}
{{eqn | l = \map {\RR^\gets} {\set 0}
      | r = \set 0
      | c = 
}}
{{eqn | l = \map {\RR^\gets} {\set 1}
      | r = \set 0
      | c = 
}}
{{eqn | l = \map {\RR^\gets} {\set {0, 1} }
      | r = \set 0
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Direct Image Mappings
Category:Inverse Image Mappings
3xmc2wkc6fh79s80i6l6agnrh857act
Theorem: Equivalence of Definitions of Maximal Element

Let $\struct {S, \RR}$ be a relational structure.
Let $T \subseteq S$ be a subset of $S$.
{{TFAE|def = Maximal Element}}

Proof:
=== Definition 1 implies Definition 2 ===
Let $x$ be an maximal element by definition 1.
That is:
:$(1): \quad \forall y \in T: x \mathrel \RR y \implies x = y$
{{AimForCont}} that:
:$\exists y \in T: x \mathrel {\RR^\ne} y$
Then by definition:
:$x \mathrel \RR y \land x \ne y$
which contradicts $(1)$.
Thus by Proof by Contradiction:
:$\nexists y \in T: x \mathrel {\RR^\ne} y$
That is $x$ is a maximal element by definition 2.
{{qed|lemma}}
Theorem: Equivalence of Definitions of Minimal Element

Let $\struct {S, \RR}$ be a relational structure.
Let $T \subseteq S$ be a subset of $S$.
{{TFAE|def = Minimal Element}}

Proof:
=== Definition 1 implies Definition 2 ===
Let $x$ be an minimal element by definition 1.
That is:
:$(1): \quad \forall y \in T: y \mathrel \RR x \implies x = y$
{{AimForCont}}:
:$\exists y \in T: y \mathrel {\RR^\ne} x$
Then by definition:
:$y \mathrel \RR x \land x \ne y$
which contradicts $(1)$.
Thus by Proof by Contradiction:
:$\nexists y \in T: y \mathrel {\RR^\ne} x$
That is $x$ is a minimal element by definition 2.
{{qed|lemma}}
Theorem: Singleton of Power Set less Empty Set is Minimal Subset

Let $S$ be a set which is non-empty.
Let $\CC = \powerset S \setminus \O$, that is, the power set of $S$ without the empty set.
Let $x \in S$.
Then $\set x$ is a minimal element of the ordered structure $\struct {\CC, \subseteq}$.

Proof:
Let $y \in \CC$ such that $y \subseteq \set x$.
We have that $\O \notin \CC$.
Therefore:
:$\exists z \in S: z \in y$
But as $y \subseteq \set x$ it follows that:
:$z \in \set x$
and so by definition of singleton:
:$z = x$
and so:
:$y = \set x$
and so:
:$y = x$
Thus, by definition, $\set x$ is a minimal element of $\struct {\CC, \subseteq}$.
{{qed}}
Theorem: Power Set less Empty Set has no Smallest Element iff not Singleton

Let $S$ be a set which is non-empty.
Let $\CC = \powerset S \setminus \O$, that is, the power set of $S$ without the empty set.
Then the ordered structure $\struct {\CC, \subseteq}$ has no smallest element {{iff}} $S$ is not a singleton.

Proof:
=== Necessary Condition ===
Let $S$ not be a singleton.
Then $\exists x, y \in S: x \ne y$.
Let $Z \in \CC$ be the smallest element of $\CC$.
Then:
:$\forall T \in \CC: Z \subseteq T$
But by Singleton of Power Set less Empty Set is Minimal Subset, both $\set x$ and $\set y$ are minimal elements of $\struct {\CC, \subseteq}$.
Therefore it cannot be the case that $Z \subseteq \set x$ and $Z \subseteq \set y$.
Therefore $\struct {\CC, \subseteq}$ has no smallest element.
{{qed|lemma}}
Theorem: Natural Numbers under Multiplication form Semigroup

Let $\N$ be the set of natural numbers.
Let $\times$ denote the operation of multiplication on $\N$.
The structure $\struct {\N, \times}$ forms a semigroup.

Proof:
=== {{Semigroup-axiom|0|nolink}} ===
We have that Natural Number Multiplication is Closed.
That is, $\struct {\N, \times}$ is closed.
{{qed|lemma}}
Theorem: Non-Zero Natural Numbers under Addition form Semigroup

Let $\N_{>0}$ be the set of natural numbers without zero, that is:
:$\N_{>0} = \N \setminus \set 0$
Let $+$ denote natural number addition.
The structure $\struct {\N_{>0}, +}$ forms a semigroup.

Proof:
This is a specific instance of Natural Numbers Bounded Below under Addition form Commutative Semigroup.
{{qed}}
Theorem: Trisecting the Angle/Neusis Construction

Let $\alpha$ be an angle which is to be trisected.
This can be achieved by means of a neusis construction.

Proof:
We have that $\angle BCD + \angle ACB$ make a straight angle.
As $CD = AB$ by construction, $CD = BC$ by definition of radius of circle.
Thus $\triangle BCD$ is isosceles.
By Isosceles Triangle has Two Equal Angles:
:$\angle CBD = \angle CDB$
From Sum of Angles of Triangle equals Two Right Angles:
:$\angle BCD + 2 \angle CBD$ equals two right angles.
Thus:
:$2 \angle CBD = \angle ACB$
Similarly, by Isosceles Triangle has Two Equal Angles:
:$\angle ACB = \angle CAB$
and again from Sum of Angles of Triangle equals Two Right Angles:
:$\angle ABC + 2 \angle ACB$ equals two right angles.
and so:
:$\angle ABC + 4 \angle CBD$ equals two right angles.
But $\alpha + \angle ABC + \angle CBD$ make a straight angle.
Thus:
:$\alpha + \angle ABC + \angle CBD = \angle ABC + 4 \angle CBD$
and so:
:$\alpha = 3 \angle CBD$
{{qed}}
Theorem: Trisecting the Angle by Compass and Straightedge Construction is Impossible

There is no compass and straightedge construction for the trisection of the general angle.

Proof:
Let $OA$ and $OB$ intersect at $O$.
It will be shown that there is no general method using a compass and straightedge construction to construct $OC$ such that $\angle AOB = 3 \times \angle AOC$.
It is sufficient to demonstrate that this is impossible for one specific angle.
Hence we choose $\angle AOB = 60 \degrees$.
Let $A$ and $B$ be points on the unit circle whose center is at $\tuple {0, 0}$.
Let $A$ lie on the $x$-axis.
Thus:
:$O$ is the point $\tuple {0, 0}$
:$A$ is the point $\tuple {1, 0}$
:$B$ is the point $\tuple {\cos 60 \degrees, \sin 60 \degrees}$
These all belong to $\Q \sqbrk {\sqrt 3}$.
trisection of $AOB$ is equivalent to constructing the point $\tuple {\cos 20 \degrees, \sin 20 \degrees}$.
From Triple Angle Formula for Cosine:
:$\cos 3 \theta = 4 \cos^3 \theta - 3 \cos \theta$
so:
:$8 \cos^3 20 \degrees - 6 \cos 20 \degrees = 2 \cos 60 \degrees = 1$
Thus $\cos 20 \degrees$ is a root of the polynomial:
:$8 x^3 = 6 x - 1$
which by Irreducible Polynomial: $8 x^3 - 6 x - 1$ in Rationals is irreducible over $\Q$.
Thus $\cos 20 \degrees$ is algebraic over $\Q$ with degree $3$.
Thus by Algebraic Element of Degree 3 is not Element of Field Extension of Degree Power of 2, $\cos 20 \degrees$ is not an element of any extension of $\Q$ of degree $2^m$.
The result follows from Point in Plane is Constructible iff Coordinates in Extension of Degree Power of 2.
{{qed}}
Theorem: Doubling the Cube by Compass and Straightedge Construction is Impossible

There is no compass and straightedge construction to allow a cube to be constructed whose volume is double that of a given cube.

Proof:
Suppose it is possible.
Then from a cube of edge length $L$ we can construct a new cube with edge length $\sqrt [3] 2 L$.
$\sqrt [3] 2$ is algebraic of degree $3$.
This contradicts Constructible Length with Compass and Straightedge.
{{qed}}
Theorem: Squaring the Circle by Compass and Straightedge Construction is Impossible

There is no compass and straightedge construction to allow a square to be constructed whose area is equal to that of a given circle.

Proof:
Squaring the Circle consists of constructing a line segment of length $\sqrt \pi$ of another.
From Constructible Length with Compass and Straightedge, any such line segment has a length which is an algebraic number of degree $2$.
But $\pi$ is transcendental.
Hence $\pi$ and therefore $\sqrt \pi$ is not such an algebraic number.
Therefore any attempt at such a construction will fail.
{{Qed}}
Theorem: Time Taken for Body to Fall at Earth's Surface

Let an object $m$ be released above ground from a point near the Earth's surface and allowed to fall freely.
Let $m$ fall a distance $s$ in time $t$.
Then:
:$s = \dfrac 1 2 g t^2$
or:
:$t = \sqrt {\dfrac {2 s} g}$
where $g$ is the Acceleration Due to Gravity at the height through which $m$ falls.
It is supposed that the distance $s$ is small enough that $g$ can be considered constant throughout.

Proof:
From Equations of Motion with Constant Acceleration: Distance after Time:
:$\mathbf s = \mathbf u t + \dfrac {\mathbf a t^2} 2$
Here the body falls from rest, so:
:$\mathbf u = \mathbf 0$
Thus:
:$\mathbf s = \dfrac {\mathbf g t^2} 2$
and so taking magnitudes:
:$s = \dfrac {g t^2} 2$
It follows by multiplying by $\dfrac 2 g$ that:
:$t^2 = \dfrac {2 s} g$
whence:
:$t = \sqrt {\dfrac {2 s} g}$
{{qed}}
Theorem: Length of Chord of Circle

Let $C$ be a circle of radius $r$.
Let $AB$ be a chord which joins the endpoints of the arc $ADB$.
Then:
:$AB = 2 r \sin \dfrac \theta 2$
where $\theta$ is the angle subtended by $AB$ at the center of $C$.

Proof:
:300px
Let $O$ be the center of $C$.
Let $AB$ be bisected by $OD$.
Consider the pair of triangles $\triangle AOE$ and $\triangle BOE$.
We see that:
:$AE = EB$ since $AB$ is bisected by $OD$
:$AO = BO$ since they are radii
:$OE = OE$ since they are common sides.
By Triangle Side-Side-Side Congruence:
:$\triangle AOE = \triangle BOE$
Then we have:
:$\angle AOE = \angle BOE = \dfrac \theta 2$
:$\angle OEA = \angle OEB = \dfrac {180 \degrees} 2 = 90 \degrees$
By {{Defof|Sine Function}}:
:$\sin \dfrac \theta 2 = \dfrac {AE} {AO} = \dfrac {\frac 1 2 AB} r$
Rearranging, we get:
:$AB = 2 r \sin \dfrac \theta 2$
as desired.
{{qed}}
Theorem: Length of Chord of Circle

Let $C$ be a circle of radius $r$.
Let $AB$ be a chord which joins the endpoints of the arc $ADB$.
Then:
:$AB = 2 r \sin \dfrac \theta 2$
where $\theta$ is the angle subtended by $AB$ at the center of $C$.

Proof:
We have $AO = BO$ since they are radii.
Therefore $\triangle AOB$ is isosceles.
By Isosceles Triangle has Two Equal Angles:
:$\angle OAB = \angle OBA$
By Sum of Angles of Triangle equals Two Right Angles:
:$\angle OAB + \angle OBA + \theta = 180 \degrees$
Therefore $\angle OAB = \dfrac {180 \degrees - \theta} 2 = 90 \degrees - \dfrac \theta 2$.
Thus:
{{begin-eqn}}
{{eqn | l = \dfrac {AB} {\sin \theta}
      | r = \dfrac {BO} {\sin \angle OAB}
      | c = Law of Sines
}}
{{eqn | l = {AB}
      | r = \dfrac {BO \sin \theta} {\sin \angle OAB}
      | c = 
}}
{{eqn | r = \dfrac {2 r \sin \frac \theta 2 \cos \frac \theta 2} {\map \sin {90 \degrees - \frac \theta 2} } 
      | c = Double Angle Formula for Sine
}}
{{eqn | r = \dfrac {2 r \sin \frac \theta 2 \cos \frac \theta 2} {\cos \frac \theta 2}
      | c = Sine of Supplementary Angle
}}
{{eqn | r = 2 r \sin \dfrac \theta 2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Ptolemy's Theorem

Let $ABCD$ be a cyclic quadrilateral.
Then:
:$AB \times CD + AD \times BC = AC \times BD$

Proof:
250px
Let $\Box ABCD$ be a cyclic quadrilateral, with diagonals $AC$ and $BD$.  
By Opposite Angles of Cyclic Quadrilateral sum to Two Right Angles:
:$\angle ABC$ is supplementary to $\angle ADC$
As well:
:$\angle BAD$ is supplementary to $\angle BCD$
Construct two triangles $\triangle A'B'C'$ and $\triangle C'D'E'$ congruent to $\triangle ABC$ and $\triangle CDE$ respectively, with $B'C'D'$ collinear.
400px
{{improve|This is messy. The new triangles have different points, so we can't refer to them as $\triangle ABC$ and $\triangle CDE$. We also need to be more precise about exactly what we are doing, because currently it's woolly.}}
$E$ is the same point that was $A$ in Figure $1$.
Hence:
:$ED = AD$
$\angle ABC$ and $\angle CDE$ are supplementary.
By Equal Corresponding Angles or Supplementary Interior Angles implies Parallel Lines:
:$AB \parallel ED$
By construction:
:$AC = EC$
Now, scale the sides of $\triangle CDE$ by the length of $AB$.
Also scale the sides of $\triangle ABC$ by the length of $DE$.
600px
Let the scaled figure be $A'B'F'G'$.
:$A'B' = AB \cdot DE = F'G'$
By Quadrilateral is Parallelogram iff One Pair of Opposite Sides is Equal and Parallel:
:$\Box A'B'F'G'$ is a parallelogram
By construction:
:$\angle A'C'B' + \angle A'C'F'$ has the same measure of angle as the original $\angle BCD$.
Therefore the supplementary angle $\angle A'C'G'$ has the same measure as the supplementary angle $\angle BAD$. 
By construction:
:$A'C' = AC \times DE$
:$B'C' = BC \times DE$
Also by construction:
:$C'G' = CE \times AC = AD \cdot AC$
:$C'F' = CD \times AC$
Therefore $A'C'$ and $C'G'$ are in proportion with scale factor $AC$.
By Triangles with One Equal Angle and Two Sides Proportional are Similar:
:$\triangle A'C'H' \sim \triangle ABD$
Thus, the length of $A'G'$ of the new construct is equal to $BD$ times the scale factor $AC$ Euclid:Proposition/VI/4:
:$A'G' = AC \times BD$
And:
:$B'F' = B'C' + C'F'$
Substituting:
:$B'F' = BC \times DE + CD \times AC$
But by Opposite Sides and Angles of Parallelogram are Equal: 
:$A'G' = B'C'F' = B'F'$
Therefore 
:$AC \times BD = BC \times DE + CD \times AC$
{{qed}}