avewright/proofwiki-math huggingface dataset:
Theorem: Undecidability Theorem

Let $T$ be the set of theorems of some consistent theory in the language of arithmetic which contains minimal arithmetic $Q$.
Then $T$ is not recursive.

Proof:
Let $\Theta$ be the set of Gödel numbers of the theorems in $T$.
We have that $T$ is a consistent extension of $Q$.
By Set of Gödel Numbers of Arithmetic Theorems Not Definable in Arithmetic, $\Theta$ is not a definable set in $T$.
Since Recursive Sets are Definable in Arithmetic, this means that $\Theta$ is not recursive.
{{AimForCont}} $T$ were recursive.
Then by Gödel Numbering is Recursive, we could recursively go from $\Theta$ to $T$.
Then using the recursivity of $T$, we could then recursively go back to $\Theta$.
Thus $\Theta$ would be recursive.
This would be a contradiction.
Thus, by Proof by Contradiction, $T$ is not recursive.
{{qed}}
Theorem: Set of Gödel Numbers of Arithmetic Theorems Not Definable in Arithmetic

Let $T$ be the set of theorems of some consistent theory in the language of arithmetic which contains minimal arithmetic.
The set of Gödel numbers of the theorems of $T$ is not definable in $T$.

Proof:
{{Questionable|Not only the proof is faulty, this theorem is wrong. If we have a recursively enumerable set A of axioms, then the set of theorems (and hence, the Gödel numbers of those) proven by A is recursively enumerable. Minimal arithmetic and PA are both recursively enumerable, and hence their theorems have a recursively enumerable set of Gödel numbers. Any recursively enumerable set is arithmetical with degree Sigma^0_1 in the arithmetical hierarchy. Moreover, there is already a well known provability predicate Pr(x) in the language of Peano arithmetic. Indeed, if we use the diagonal lemma on ~Pr(x) to get a sentence with T proves G iff ~Pr(G), then we will have an unprovable sentence.|Burak}}
The proof is by contradiction.
Let $\Theta$ be the set of Gödel numbers of the theorems of $T$.
Suppose it is defined in $T$ by the formula $\map \theta y$.
Since $T$ contains $Q$, we may apply the Diagonal Lemma to $\neg \map \theta y$.
This gives us a sentence $G$ such that
:$T \vdash G \leftrightarrow \neg \map \theta {\hat G}$
where $\hat G$ is the Gödel number of $G$ (more accurately, it is the term in the language of arithmetic obtained by applying the function symbol $s$ to $0$ this many times).
{{Questionable|The below argument is not correct. $T$ does not necessarily prove that $\neg \map \theta {\hat G}$ just because it does not prove $G$. PA has a provability predicate $\map \Pr x$ which satisfies the property that if PA proves G, then PA proves $\map \Pr {\hat G}$). The step used here assumes a somewhat similar property in the opposite direction that our provability predicate satisfies if T does not prove G, then T proves $\neg \map \theta {\hat G}$, which we did not have as an assumption on $\map \Theta x$. |Burak}}
Suppose $G$ is not a theorem of $T$.
:Then the Gödel number of $G$ is not in $\Theta$.
:Since $\theta$ defines $\Theta$ in $T$, this means that:
::$T \vdash \neg \map \theta {\hat G}$
:But, by choice of $G$ (specifically, the bi-implication above), this gives us:
::$T\vdash G$
:which contradicts $G$ not being a theorem of $T$
Thus, $G$ is a theorem of $T$.
:But, then the Gödel number of $G$ is in $\Theta$, and
:since $\theta$ defines $\Theta$ in $T$, this means that
::$T \vdash \map \theta {\hat G}$
:But, then this gives us
::$T \vdash \neg G$
:which contradicts $G$ being a theorem of $T$, ''since $T$ is consistent''.
Since assuming $\Theta$ was definable in $T$ necessarily leads to a contradiction, we conclude that it is impossible.
{{qed}}
Theorem: Diagonal Lemma

Let $T$ be the set of theorems of some theory in the language of arithmetic which contains minimal arithmetic.
For any formula $\map B y$ in the language of arithmetic, there is a sentence $G$ such that
:$T \vdash G \leftrightarrow \map B {\hat G}$
where $\hat G$ is the Gödel number of $G$ (more accurately, it is the term in the language of arithmetic obtained by applying the function symbol $s$ to $0$ this many times).
{{Disambiguate|Definition:Logical Formula}}

Proof:
There is a primitive recursive function $\mathrm {diag}$ which is defined by:
:$\map {\mathrm {diag} } n = \widehat {\map A {\hat A} }$
where:
:$\map A x$ is the formula such that $\hat A = n$.
:the $\hat {}$ sign denotes the Gödel number of the contained formula (and we are not being formal about distinguishing between integers and symbols in the language).
Informally, $\mathrm {diag}$ takes a Gödel number, decodes it to a formula, plugs in the Gödel number for that formula in place of a free variable, and encodes this new formula back to a new Gödel number.
Since $T$ contains $Q$, by Recursive Sets are Definable in Arithmetic applied to the graph of $\mathrm {diag}$, we have that there is some formula $\map {\mathrm {Diag} } {x, y}$ which defines the graph of $\mathrm {diag}$ in $T$.
That is:
:$\map {\mathrm {diag} } n = m$ {{iff}} $T \vdash \map {\mathrm {Diag} } {n, m}$
Let $\map A x$ be the formula:
:$\exists y \paren {\map {\mathrm {Diag} } {x, y} \land \map B y}$
Let $G$ be $\map A {\hat A}$.
We then have $T \vdash \map {\mathrm {Diag} } {\hat A, \hat G}$, by checking the definitions.
Let $T' = T \cup \set G$.
Then:
:$T' \vdash \map A {\hat A}$
Hence:
:$T' \vdash \exists y \paren {\map {\mathrm {Diag} } {\hat A, y} \land \map B y}$
But since $\hat G$ is the only number such that $T \vdash \map {\mathrm {Diag} } {\hat A, \hat G}$, this gives us:
:$T' \vdash \map B {\hat G}$
Thus:
:$T \vdash G \rightarrow \map B {\hat G}$
Let $T' = T \cup \set {\map B {\hat G} }$.
Again, we have:
:$T \vdash \map {\mathrm {Diag} } {\hat A, \hat G}$
so this gives us:
:$T' \vdash \map {\mathrm {Diag} } {\hat A, \hat G} \land \map B {\hat G}$
and hence:
:$T' \vdash \exists y \paren {\map {\mathrm {Diag} } {\hat A, y} \land \map B y}$
But this is the same thing as:
:$T' \vdash G$
Thus:
:$T \vdash \map B {\hat G} \rightarrow G$
Thus $G$ is as claimed.
{{qed}}
{{MissingLinks|first line of proof}}
Theorem: Tarski's Undefinability Theorem

Let $\ZZ$ be the standard structure $\struct {\Z, +, \cdot, s, <, 0}$ for the language of arithmetic.
Let $\operatorname {Th}_\ZZ$ be the sentences which are true in $\ZZ$.
Let $\Theta$ be the set of Gödel numbers of those sentences in $\operatorname {Th}_\ZZ$.
$\Theta$ is not definable in $\operatorname {Th}_\ZZ$.

Proof:
$\operatorname {Th}_\ZZ$ is easily seen to be a consistent extension of minimal arithmetic.  (In fact, the axioms in minimal arithmetic were selected based on the behavior of standard arithmetic.)
Thus, the theorem is a special case of Set of Gödel Numbers of Arithmetic Theorems Not Definable in Arithmetic (and can be seen to follow immediately).
{{qed}}
{{Namedfor|Alfred Tarski|cat = Tarski}}
Theorem: Equivalence of Definitions of Limit Point of Set

Let $T = \struct {S, \tau}$ be a topological space.
Let $A \subseteq S$.
{{TFAE|def = Limit Point of Set|view = a limit point of a set}}
=== Definition from Open Neighborhood===
{{:Definition:Limit Point of Set/Definition from Open Neighborhood}}
=== Definition from Closure===
{{:Definition:Limit Point of Set/Definition from Closure}}
=== Definition from Adherent Point===
{{:Definition:Limit Point of Set/Definition from Adherent Point}}
=== Definition from Relative Complement===
{{:Definition:Limit Point of Set/Definition from Relative Complement}}

Proof:
=== Definition from Open Neighborhood $\iff$ Definition from Closure ===
The closure of $A$ is defined as the union of the set of all isolated points of $A$ and the set of all limit points of $A$.
The rest then follows directly from Equivalence of Definitions of Isolated Point.
{{qed|lemma}}
Theorem: Equivalence of Definitions of Limit Point of Set

Let $T = \struct {S, \tau}$ be a topological space.
Let $A \subseteq S$.
{{TFAE|def = Limit Point of Set|view = a limit point of a set}}
=== Definition from Open Neighborhood===
{{:Definition:Limit Point of Set/Definition from Open Neighborhood}}
=== Definition from Closure===
{{:Definition:Limit Point of Set/Definition from Closure}}
=== Definition from Adherent Point===
{{:Definition:Limit Point of Set/Definition from Adherent Point}}
=== Definition from Relative Complement===
{{:Definition:Limit Point of Set/Definition from Relative Complement}}

Proof:
The following equivalence holds:
{{begin-eqn}}
{{eqn | o =
      | c = There exists an open neighborhood $U$ of $x$ such that $A \cap \paren {U \setminus \set x} = \O$
}}
{{eqn | o = \leadstoandfrom
      | c = There exists an open neighborhood $U$ of $x$ such that $U \subseteq \paren{S \setminus A} \cup \set x$
      | cc = Modus Ponendo Tollens
}}
{{eqn | o = \leadstoandfrom
      | c = $\paren {S \setminus A} \cup \set x$ is a neighborhood of $x$
      | cc = {{Defof|Neighborhood of Point}}
}}
{{end-eqn}}
The result follows from the Rule of Transposition.
{{qed}}
Theorem: Equivalence of Definitions of Limit Point of Set

Let $T = \struct {S, \tau}$ be a topological space.
Let $A \subseteq S$.
{{TFAE|def = Limit Point of Set|view = a limit point of a set}}
=== Definition from Open Neighborhood===
{{:Definition:Limit Point of Set/Definition from Open Neighborhood}}
=== Definition from Closure===
{{:Definition:Limit Point of Set/Definition from Closure}}
=== Definition from Adherent Point===
{{:Definition:Limit Point of Set/Definition from Adherent Point}}
=== Definition from Relative Complement===
{{:Definition:Limit Point of Set/Definition from Relative Complement}}

Proof:
The following equivalence holds:
There exists an open neighborhood $U$ of $x$ such that $A \cap \paren {U \setminus \set x} = \O$
{{begin-eqn}}
{{eqn | l = \O
      | r = A \cap \paren {U \setminus \set x}
}}
{{eqn | ll = \leadstoandfrom
      | l  = \O
      | r  = \paren {U \cap A} \setminus \set x
      | cc = Intersection with Set Difference is Set Difference with Intersection
}}
{{eqn | ll = \leadstoandfrom
      | l  = \O
      | r  = \paren {A \cap U} \setminus \set x
      | cc = Intersection is Commutative
}}
{{eqn | ll = \leadstoandfrom
      | l  = \O
      | r  = U \cap \paren {A \setminus \set x}
      | cc = Intersection with Set Difference is Set Difference with Intersection
}}
{{eqn | ll = \leadstoandfrom
      | l  = \O
      | r  = U \cap \map \complement {\map \complement {A \setminus \set x} }
      | cc = Complement of Complement
}}
{{eqn | ll = \leadstoandfrom
      | l  = U
      | o  = \subseteq
      | r  = \map \complement {A \setminus \set x}
      | cc = Intersection with Complement is Empty iff Subset
}}
{{eqn | ll = \leadstoandfrom
      | l  = U
      | o  = \subseteq
      | r  = \map \complement {A \cap \map \complement {\set x} }
      | cc = Set Difference as Intersection with Complement
}}
{{eqn | ll = \leadstoandfrom
      | l  = U
      | o  = \subseteq
      | r  = \map \complement A \cup \map \complement {\map \complement {\set x} }
      | cc = De Morgan's Laws (Set Theory)/Set Complement
}}
{{eqn | ll = \leadstoandfrom
      | l  = U
      | o  = \subseteq
      | r  = \map \complement A \cup \set x
      | cc = Complement of Complement
}}
{{end-eqn}}
By {{Defof|Neighborhood of Point}}, $\map \complement A \cup \set x$ is a neighborhood of $x$
The result follows from the Rule of Transposition.
{{qed}}
Theorem: Denseness Preserved in Coarser Topology

Let $T = \struct {S, \tau}$ be a topological space.
Let $T' = \struct {S, \tau'}$ be another topological space on $S$ such that $\tau'$ is coarser than $\tau$.
Let $H \subseteq S$ be everywhere dense in $T$.
Then $H$ is also everywhere dense in $T'$.

Proof:
Let $H \subseteq S$ be everywhere dense in $T$. 
As $\tau'$ is coarser than $\tau$, by definition $\tau' \subseteq \tau$.
Let $x \in S$.
As $H \subseteq S$ is everywhere dense in $T$, either $x \in H$ or $x$ is a limit point of $H$ in $T$.
Suppose $x \notin H$.
Then $x$ is a limit point of $H$ in $T$.
Then by definition of limit point of $H$:
:$\forall U \in \tau, x \in U: \exists y \in H: y \in U, y \ne x$ 
As $\tau' \subseteq \tau$ we have that $U \in \tau' \implies U \in \tau$.
So:
:$\forall U \in \tau', x \in U: \exists y \in H: y \in U, y \ne x$ 
That is, $x$ is a limit point of $H$ in $T\ '$.
As $x$ is arbitrary, this follows for all $x \in S, x \notin H$.
So, for all $x \in S$, either $x \in H$ or $x$ is a limit point of $H$ in $T'$.
Thus, by definition, $H \subseteq S$ is everywhere dense in $T'$.
{{qed}}
Category:Denseness
js5kepz4ph9o4ylhmlhwnvpvqnnonr1
Theorem: Rationals are Everywhere Dense in Compact Complement Space

Let $T = \struct {\R, \tau^*}$ be the compact complement space on $\R$.
Let $\Q$ be the set of rational numbers.
Then $\Q$ is everywhere dense in $T$.

Proof:
We have that the Compact Complement Topology is Coarser than Euclidean Topology.
The result follows from Denseness Preserved in Coarser Topology.
{{qed}}
Theorem: Compact Complement Topology is Separable

Let $T = \struct {\R, \tau}$ be the compact complement topology on $\R$.
Then $T$ is a separable space.

Proof:
We have:
: Compact Complement Topology is Second-Countable
: Second-Countable Space is Separable
Hence the result.
{{qed}}
Theorem: Compact Complement Topology is Separable

Let $T = \struct {\R, \tau}$ be the compact complement topology on $\R$.
Then $T$ is a separable space.

Proof:
{{Recall|Separable Space|separable space}}
{{:Definition:Separable Space}}
We have that:
:Rationals are Everywhere Dense in Compact Complement Space
:Rational Numbers are Countably Infinite
Hence the result by definition of separable space.
{{qed}}
Theorem: Either-Or Topology is Locally Connected

Let $T = \struct {S, \tau}$ be the either-or space.
Then $T$ is a locally connected space.

Proof:
:Either-Or Topology is Locally Path-Connected
:Locally Path-Connected Space is Locally Connected
{{qed}}
Theorem: Either-Or Topology is not Locally Injectively Path-Connected

Let $T = \struct {S, \tau}$ be the either-or space.
Then $T$ is not a locally injectively path-connected space.

Proof:
Let $\BB$ be a basis for $\tau$.
Suppose that $0 \in B$, where $B \in \BB$.
Then by definition of the either-or topology, $\openint {-1} 1 \subseteq B$.
In particular, $\dfrac 1 2 \in B$.
Let $f: \closedint 0 1 \to B$ be an arbitrary injection such that:
{{begin-eqn}}
{{eqn | l = \map f 0
      | r = 0
}}
{{eqn | l = \map f 1
      | r = \dfrac 1 2
}}
{{end-eqn}}
Since $0 \notin \set {\dfrac 1 2}$, it follows that $\set {\dfrac 1 2}$ is open in $\tau$.
As $f$ is an injection, it follows that:
:$f^{-1} \sqbrk {\set {\dfrac 1 2} } = \set 1$
By Closed Real Interval is not Open Set, $\set 1 = \closedint 1 1$ is not open in $\closedint 0 1$.
Thus, $f$ cannot be continuous.
Hence, no injective path from $0$ to $\dfrac 1 2$ can exist.
It follows that $B$ is not injectively path-connected, and hence $T$ is not locally injectively path-connected.
{{qed}}
Theorem: Limit Points in Uncountable Fort Space

Let $T = \struct {S, \tau_p}$ be an uncountable Fort space.
Let $U \subseteq S$ be a countably infinite subset of $S$.
Then $p$ is the only limit point of $U$.

Proof:
Suppose $y \in S, y \ne p$.
We have by definition of Fort space that $\set y$ is open in $T$.
So there is no $z \in \set y: z \ne y, z \in U$. 
Hence $y$ can not be a limit point of $U$.
Suppose $p \in V \in \tau_p$ for some $V \subseteq S$.
From {{Defof|Fort Space}}, $\relcomp S V$ is finite.
Then:
{{begin-eqn}}
{{eqn | l = \relcomp S {V \setminus \set p}
      | r = \paren {\relcomp S V} \cup \paren {V \cap \set p}
      | c = Set Difference with Set Difference is Union of Set Difference with Intersection
}}
{{eqn | o = \subseteq 
      | r = \paren {\relcomp S V} \cup \set p
      | c = Set Union Preserves Subsets: $V \cap \set p \subset \set p$: Intersection is Subset
}}
{{end-eqn}}
Thus $\relcomp S {V \setminus \set p}$ is also finite.
Since $U$ is countably infinite:
:$U \nsubseteq \relcomp S {V \setminus \set p}$.
From Empty Intersection iff Subset of Complement:
:$U \cap \paren {V \setminus \set p} \ne \O$.
Since $V$ is arbitrary, every open neighborhood of $p$ has non-empty intersection with $U$.
Thus $p$ is the only limit point of $U$.
{{qed}}
Theorem: Fort Space is Scattered

Let $T = \struct {S, \tau_p}$ be a Fort space on an infinite set $S$.
Then $T$ is a scattered space.

Proof:
Let $H \subseteq T$ such that $H \ne \O$ and $H \ne \set p$.
Then $\exists x \in H: x \ne p$.
From Clopen Points in Fort Space, every point of $T$ apart from $p$ is open in $T$.
So $\set x$ is an open set of $T$.
So $H \cap \set x = \set x$ and so $x$ is isolated in $H$.
Thus $H$ contains at least one point which is isolated in $H$.
On the other hand, suppose $H = \set p$.
From Singleton Point is Isolated, $p$ is an isolated point in $\set p = H$.
So again $H$ contains at least one point which is isolated in $H$.
So for all $H \subseteq S$ we have that $H$ contains at least one point which is isolated in $H$.
Hence the result, by definition of scattered space.
{{qed}}
Theorem: Fort Space is Scattered

Let $T = \struct {S, \tau_p}$ be a Fort space on an infinite set $S$.
Then $T$ is a scattered space.

Proof:
{{Recall|Scattered Space|scattered space}}
{{:Definition:Scattered Space/Definition 1}}
{{AimForCont}} $H \subseteq T$ has no isolated points of $H$.
So, by definition, $H$ is dense in itself.
We have that:
:a Fort Space is $T_1$
:a Dense-in-itself Subset of $T_1$ Space is Infinite.
So $H$ is infinite, and so contains more than one point.
So:
:$\exists q \in H: q \ne p$
But, from Clopen Points in Fort Space, $\set q$ is open in $T$.
So $H \cap \set q = \set q$ and so by definition $q$ is isolated in $H$.
From this contradiction it follows that $H$ is not dense-in-itself and contains at least one isolated point.
Hence the result, by definition of scattered space.
{{qed}}
Theorem: Dense-in-itself Subset of T1 Space is Infinite

Let $T = \struct {S, \tau_p}$ be a $T_1$ space.
Let $H \subseteq T$ be dense-in-itself.
Then $H$ is infinite.

Proof:
;Proof by Contradiction
{{AimForCont}} $H$ is finite.
From Finite $T_1$ Space is Discrete, $H$ has the discrete topology.
From Discrete Space is not Dense-In-Itself it then follows that $H$ can not be dense-in-itself.
So for $H$ to be dense-in-itself, it must be infinite.
{{qed}}
Theorem: Equal Chords in Circle

In a circle, equal chords are equally distant from the center, and chords that are equally distant from the center are equal in length.
{{:Euclid:Proposition/III/14}}

Proof:
:300px
Let $ABDC$ be a circle, and let $AB$ and $CD$ be equal chords on it.
From Finding Center of Circle, let $E$ be the center of $ABDC$.
Construct $EF$, $EG$ perpendicular to $AB$ and $CD$, and join $AE$ and $EC$.
From Conditions for Diameter to be Perpendicular Bisector, $EF$ bisects $AD$.
So $AF = FB$ and so $AB = 2 AF$.
Similarly $CD = 2CG$.
As $AB = CD$ it follows that $AE = CG$.
Since $AE = EC$ the square on $AE$ equals the square on $EC$.
We have that $\angle AFE$ is a right angle.
So from Pythagoras's Theorem the square on $AE$ equals the sum of the squares on $AF$ and $FE$.
Similarly, the square on $EC$ equals the sum of the squares on $EG$ and $GC$.
Thus the square on $EF$ equals the square on $EG$.
So $EF = EG$.
So from Definition III: 4, chords are at equal distance from the center when the perpendiculars drawn to them from the center are equal.
So $AB$ and $CD$ are at equal distance from the center.
{{qed|lemma}}
Now suppose that $AB$ and $CD$ are at equal distance from the center.
That is, let $EF = EG$.
Using the same construction as above, it is proved similarly that $AB = 2AF$ and $CD = 2CG$.
Since $AE = CE$, the square on $AE$ equals the square on $CE$.
From Pythagoras's Theorem:
: the square on $AE$ equals the sum of the squares on $AF$ and $FE$
: the square on $EC$ equals the sum of the squares on $EG$ and $GC$.
So the sum of the squares on $AF$ and $FE$ equals the sum of the squares on $EG$ and $GC$.
But the square on $FE$ equals the square on $EG$.
So the square on $AF$ equals the square on $CG$, and so $AF = CG$.
As $AB = 2AF$ and $CD = 2CG$ it follows that $AB = CD$.
Hence the result.
{{qed}}
{{Euclid Note|14|III}}
Theorem: Relative Lengths of Chords of Circles

Of chords in a circle, the diameter is the greatest, and of the rest the nearer to the center is always greater than the more remote.
{{:Euclid:Proposition/III/15}}

Proof:
:320px
Let $ABCD$ be a clrcle, let $AD$ be its diameter and $E$ the center.
Let $BC$ and $FG$ be chords of $ABCD$, where $BC$ is nearer to the center than $FG$.
Let $EH$ and $EK$ be drawn perpendicular to $BC$ and $FG$ respectively.
Because $BC$ is nearer to the center than $FG$, it follows from Book III: Definition 5 that $EK$ is longer than $EH$.
Position $L$ on $EK$ so that $EL = EH$, and draw $MN$ through $L$ perpendicular to $FG$.
Join $EM$, $EN$, $EF$ and $EG$.
Since $EH = EL$ it follows from Equal Chords in Circle that $BC = MN$.
Also, since $AE = EM$ and $ED = EN$, $AD = ME + EN$.
But $ME + EN > MN$ from Sum of Two Sides of Triangle Greater than Third Side, and $MN = BC$.
So $AD > BC$.
Thus we have that the diameter is greater than any other chord of a circle.
{{qed|lemma}}
Since $ME = FE$ and $EN = EG$ and $\angle MEN > \angle FEG$, from the Hinge Theorem it follows that $MN > FG$.
But $MN = BC$.
So a chord nearer the center is greater than one more remote.
{{qed}}
{{Euclid Note|15|III}}
Theorem: Construction of Tangent from Point to Circle

From a given point outside a given circle, it is possible to draw a tangent to that circle.
{{:Euclid:Proposition/III/17}}

Proof:
:400px
Let $A$ be the given point and let $BCD$ be the given circle.
It is required that a straight line be drawn from $A$ to $BCD$.
Let the center $E$ of $BCD$ be found.
Join $AE$ and draw the circle $AFG$ with center $E$ and radius $AE$.
From $D$ let $DF$ be drawn perpendicular to $EA$.
Join $EF$ and let $B$ be the point at which $EF$ joins the circle $BCD$.
Join $AB$.
Then $AB$ is the required tangent to $BCD$.
=== Proof of Construction ===
Since $E$ is the center of the circles $BCD$ and $AFG$, $EA = EF$ and $ED = EB$.
Therefore the two sides $AE, EB$ equal the two sides $FE, ED$, and they contain a common angle at $E$.
So by Triangle Side-Angle-Side Congruence, $\triangle DEF = \triangle BEA$.
Therefore $\angle EDF = \angle EBA$.
But $\angle EDF$ is a right angle, so $\angle EBA$ is also a right angle.
But $EB$ is a radius of circle $BCD$.
It follows from the porism to Line at Right Angles to Diameter of Circle that $AB$ is tangent to $BCD$.
{{qed}}
Theorem: Construction of Tangent from Point to Circle

From a given point outside a given circle, it is possible to draw a tangent to that circle.
{{:Euclid:Proposition/III/17}}

Proof:
:400px
Let $BCD$ with center $A$ be the circle, and let $E$ be the exterior point from which a tangent is to be drawn.
Bisect $AE$ at $F$.
Then draw a circle $AEG$ whose center is $F$ and whose radius is $AF$.
The point $G$ is where $AEG$ intersects $BCD$.
The line $EG$ is the required tangent.
=== Proof of Construction ===
By the method of construction, $AE$ is the diameter of $AEG$.
By Thales' Theorem $\angle AGE$ is a right angle.
But $AG$ is a radius of $BCD$.
The result follows from Radius at Right Angle to Tangent.
{{qed}}
Theorem: Equal Angles in Equal Circles

In equal circles, equal angles stand on equal arcs, whether at the center or at the circumference of those circles.
{{:Euclid:Proposition/III/26}}

Proof:
Let $ABC$ and $DEF$ be equal circles.
Let $\angle BGC = \angle EHF$ and $\angle BAC = \angle EDF$.
:500px
Let $BC$ and $EF$ be joined.
Since the circles $ABC$ and $DEF$ are equal, their radii are equal.
So $BG = EH$ and $CG = FH$.
We also have {{hypothesis}} that $\angle BGC = \angle EHF$.
So from Triangle Side-Angle-Side Congruence it follows that $BC = EF$.
Since $\angle BAC = \angle EDF$ we have from {{EuclidDefLink|III|11|Similar Segments}} that segment $BAC$ is similar to segment $EDF$.
Moreover, these segments have equal bases.
So from Similar Segments on Equal Bases are Equal, segment $BAC$ is equal to segment $EDF$. 
But as $ABC$ and $DEF$ are equal circles, it follows that arc $BKC$ equals arc $ELF$.
{{qed}}
{{Euclid Note|26|III|{{EuclidNoteConverse|prop = 27|title = Angles on Equal Arcs are Equal}}}}