avewright/proofwiki-math huggingface dataset:
Theorem: Gaussian Isoperimetric Inequality

Let $A$ be a measurable subset of $\R^n$ endowed with the standard Gaussian measure $\gamma^n$ with the density $\dfrac {\map \exp {-\norm x^2 / 2} } {\paren {2 \pi}^{n/2} }$
Denote by:
:$A_\epsilon = \set {x \in \R^n: \map d {x, A} \le \epsilon}$
the $\epsilon$-extension of $A$.
The '''Gaussian isoperimetric inequality''' states that:
:$\ds \liminf_{\epsilon \mathop \to +0} \epsilon^{-1} \set {\map {\gamma^n} {A_\epsilon} - \map {\gamma^n} A} \ge \map \varphi {\map {\Phi^{-1} } {\map {\gamma^n} A } }$
where:
:$\map \varphi t = \dfrac {\map \exp {-t^2 / 2} } {\sqrt {2 \pi} }$
and:
:$\map \Phi t = \ds \int_{-\infty}^t \map \varphi s \rd s$

Proof:
{{ProofWanted}}
{{Namedfor|Carl Friedrich Gauss|cat = Gauss}}
Category:Measure Theory
fj42xkxsm5x5ffftwoxwyrazp4sw01t
Theorem: Negation of Propositional Function in Two Variables

Let $\map P {x, y}$ be a propositional function of two Variables.
Then:
:$\neg \forall x: \exists y: \map P {x, y} \iff \exists x: \forall y: \neg \map P {x, y}$
That is:
:''It is not the case that for all $x$ a value of $y$ can be found to satisfy $\map P {x, y}$''
means the same thing as:
:''There exists at least one value of $x$ such that for all $y$ it is not possible to satisfy $\map P {x, y}$''

Proof:
{{begin-eqn}}
{{eqn | q = \neg \forall x
      | l = \exists y
      | o = :
      | r = \map P {x, y}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists x
      | l = \neg \exists y
      | o = :
      | r = \map P {x, y}
      | c = Denial of Universality
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists x
      | l = \forall y
      | o = :
      | r = \neg \map P {x, y}
      | c = Denial of Existence
}}
{{end-eqn}}
{{qed}}
Theorem: Valuation Ideal of P-adic Numbers

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Then the valuation ideal induced by norm $\norm {\,\cdot\,}_p$ is the principal ideal:
:$p \Z_p = \set {x \in \Q_p: \norm x_p < 1}$
where $\Z_p$ denotes the $p$-adic integers.

Proof:
From P-adic Integers is Local Ring, $\Z_p$ is a local ring.
From Principal Ideal from Element in Center of Ring, $p \Z_p$ is a principal ideal.
Now:
{{begin-eqn}}
{{eqn | l = \norm x_p
      | o = <
      | r = 1
}}
{{eqn | ll= \leadstoandfrom 
      | l = \norm x_p
      | o = \le
      | r = \dfrac 1 p
      | c = P-adic Norm of p-adic Number is Power of p
}}
{{eqn | ll= \leadstoandfrom 
      | l = p \norm x_p
      | o = \le
      | r = 1
}}
{{eqn | ll= \leadstoandfrom 
      | l = \dfrac {\norm x_p} {\norm p_p}
      | o = \le
      | r = 1
      | c = as ${\norm p_p} = \dfrac 1 p$
}}
{{eqn | ll= \leadstoandfrom 
      | l = \norm {\dfrac x p}_p
      | o = \le
      | r = 1
      | c = Norm of Quotient
}}
{{eqn | ll= \leadstoandfrom 
      | l = \dfrac x p
      | o = \in
      | r = \Z_p
      | c = {{Defof|P-adic Integer|$p$-adic Integer}}
}}
{{eqn | ll= \leadstoandfrom 
      | l = x
      | o = \in
      | r = p \Z_p
}}
{{end-eqn}}
Hence:
:$p \Z_p = \set {x \in \Q_p: \norm x_p < 1}$
{{qed}}
Theorem: Integers are Arbitrarily Close to P-adic Integers

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $\Z_p$ be the $p$-adic integers.
Let $x \in \Z_p$.
Then for $n \in \N$ there exists unique $\alpha \in \Z$:
:$(1): \quad 0 \le \alpha \le p^n - 1$
:$(2): \quad \norm { x -\alpha}_p \le p^{-n}$

Proof:
Let $n \in \N$.
From Rational Numbers are Dense Subfield of P-adic Numbers:
:the rational numbers are dense in $\Q_p$.
So there exists:
:$\dfrac a b \in \Q: \norm {x - \dfrac a b}_p \le p^{-n}$
From Unique Integer Close to Rational in Valuation Ring of P-adic Norm,  there exists  unique $\alpha \in \Z$ such that:
:$\norm {\dfrac a b - \alpha}_p \le p^{-n}$
:$0 \le \alpha \le p^n - 1$
Then:
{{begin-eqn}}
{{eqn | l = \norm {x - \alpha}_p
      | r = \norm {\paren {x - \dfrac a b} + \paren {\dfrac a b - \alpha} }_p
}}
{{eqn | o = \le
      | r = \max \set {\norm {x - \dfrac a b}_p, \: \norm {\dfrac a b - \alpha}_p }
      | c = Norm axiom (N4) (Ultrametric Inequality)
}}
{{eqn | o = \le
      | r = p^{-n}
}}
{{end-eqn}}
Now suppose $\beta \in \Z$ also satisfies conditions $(1)$ and $(2)$, that is:
:$0 \le \beta \le p^n - 1$
:$\norm { x - \beta}_p \le p^{-n}$
Then:
{{begin-eqn}}
{{eqn | l = \norm{\dfrac a b - \beta}_p
      | r = \norm{\paren{\dfrac a b - x} + \paren{x - \beta} }_p
}}
{{eqn | o = \le
      | r = \max \set{\norm{\dfrac a b - x}_p,\:\norm{x - \beta}_p}
      | c = Norm axiom (N4) (Ultrametric Inequality)
}}
{{eqn | o = \le
      | r = \max \set{\norm{x - \dfrac a b}_p,\:\norm{x - \beta}_p}
      | c = Norm of Negative
}}
{{eqn | o = \le
      | r = p^{-n}
}}
{{end-eqn}}
From Unique Integer Close to Rational in Valuation Ring of P-adic Norm,  $\alpha \in \Z$ was unique, so:
:$\beta = \alpha$
The result follows.
{{qed}}
Theorem: Integers are Dense in P-adic Integers

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $\Z_p$ be the $p$-adic integers.
Let $d_p$ be the metric induced by the norm $\norm {\,\cdot\,}_p$ restricted to the $p$-adic integers.
The integers $\Z$ are dense in the metric space $\struct{\Z_p, d_p}$.
=== Corollary ===
{{:Integers are Dense in P-adic Integers/Unit Ball}}

Proof:
From Open Ball Characterization of Denseness it is sufficient to show that every open ball of $\struct {\Z_p, d_p}$ contains an element of $\Z$.
Let $x \in \Z_p$ and $\epsilon \in \R_{>0}$.
By definition the open ball $\map {B_\epsilon} x$ is:
:$\map {B_\epsilon} x = \set {y \in \Z_p: \norm y_p < \epsilon}$
From Sequence of Powers of Number less than One:
:$\ds \lim_{n \mathop \to \infty} p^{-n} = 0$
Hence there exists $N \in \N$:
:$\forall n \ge N: p^{-n} < \epsilon$
Consider the open ball $\map {B_{p^{-N} } } x$.
Since $0 < p^{-n} < \epsilon$ then:
:$\map {B_{p^{-N} } } x \subseteq \map {B_\epsilon} x$.
From Integers are Arbitrarily Close to $p$-adic Integers:
:$\exists \alpha \in \Z: \alpha \in \map {B_{p^{-N} } } x$
Hence $\alpha \in \map {B_\epsilon} x$.
Since $x$ and $\epsilon$ were arbitrary then every open ball of $\struct {\Z_p, d_p}$ contains an element of $\Z$.
From Open Ball Characterization of Denseness then $\Z$ is dense in the metric space $\struct {\Z_p, d_p}$.
{{qed}}
Theorem: P-adic Integer is Limit of Unique Coherent Sequence of Integers

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $\Z_p$ be the $p$-adic integers.
Let $x \in \Z_p$.
Then there exists a unique coherent sequence $\sequence {\alpha_n}$:
:$\ds \lim_{n \mathop \to \infty} \alpha_n = x$

Proof:
By the definition of a coherent sequence it needs to be proved that there exists a unique integer sequence $\sequence {\alpha_n}$:
:$(1): \quad \forall n \in \N: \alpha_n \in \Z$ and $0 \le \alpha_n \le p^{n + 1} - 1$
:$(2): \quad \forall n \in \N: \alpha_{n + 1} \equiv \alpha_n \pmod {p^{n + 1}}$
:$(3): \quad \ds \lim_{n \mathop \to \infty} \alpha_n = x$
By Integers are Arbitrarily Close to P-adic Integers then for all $n \in \N$ there exists $\alpha_n \in \Z$:
::$\text {(a)}: \quad 0 \le \alpha_n \le p^{n + 1} - 1$
::$\text {(b)}: \quad \norm {x - \alpha_n}_p \le p^{-\paren{n + 1} }$
Hence the sequence $\sequence {\alpha_n}$ satisfies $(1)$ above.
Theorem: Dimension of Vector Space on Cartesian Product

Let $\struct {K, +, \circ}$ be a division ring.
Let $n \in \N_{>0}$.
Let $\mathbf V := \struct {K^n, +, \times}_K$ be the '''$K$-vector space $K^n$'''.
Then the dimension of $\mathbf V$ is $n$.

Proof:
Let the unity of $K$ be $1$, and the zero of $K$ be $0$.
Consider the vectors:
{{begin-eqn}}
{{eqn | l = \mathbf e_1
      | o = :=
      | r = \underbrace {\tuple {1, 0, \ldots, 0} }_{n \text { coordinates} }
      | c = 
}}
{{eqn | l = \mathbf e_2
      | o = :=
      | r = \underbrace {\tuple {0, 1, \ldots, 0} }_{n \text { coordinates} }
      | c = 
}}
{{eqn | o = \vdots
      | c = 
}}
{{eqn | l = \mathbf e_n
      | o = :=
      | r = \underbrace {\tuple {0, 0, \ldots, 1} }_{n \text { coordinates} }
      | c = 
}}
{{end-eqn}}
Thus $\tuple {\mathbf e_1, \mathbf e_2, \ldots, \mathbf e_n}$ is the standard ordered basis of $\mathbf V$.
From Standard Ordered Basis is Basis, $\tuple {\mathbf e_1, \mathbf e_2, \ldots, \mathbf e_n}$ is a basis of $\mathbf V$.
The result follows from the Basis Theorem.
{{qed}}
Theorem: Dimension of Vector Space of Polynomial Functions

Let $\struct {F, +, \times}$ be a field whose unity is $1_F$.
Let $F_n \sqbrk X$ be the ring of polynomials over $F$ whose degree is less than $n$.
Then the dimension of the vector space $F_n \sqbrk X$ is $n$.

Proof:
Let $B$ be the set of all the identity functions $I^k$ on $F_n \sqbrk X$ where $n \in \Z_{\ge 0}$.
By definition, every element of $F_n \sqbrk X$ is a linear combination of $B$.
Suppose:
:$\ds \sum_{k \mathop = 0}^m \alpha_k I^k = 0, \alpha_m \ne 0$
Then by differentiating $m$ times, we obtain from Nth Derivative of Nth Power:
:$m! \alpha_m = 0$
whence $\alpha_m = 0$ which is a contradiction.
Hence $B$ is linearly independent and therefore is a basis for $F_n \sqbrk X$.
The result follows from the Basis Theorem.
{{qed}}
Theorem: Vector Space over Division Subring is Vector Space

Let $\struct {L, +_L, \times_L}$ be a division ring.
Let $K$ be a division subring of $\struct {L, +_L, \times_L}$.
Let $\struct {G, +_G, \circ}_L$ be a $L$-vector space.
Let $\circ_K$ be the restriction of $\circ$ to $K \times G$.
Hence let $\struct {G, +_G, \circ_K}_K$ be the vector space induced by $K$.
Then $\struct {G, +_G, \circ_k}_k$ is indeed a $K$-vector space.

Proof:
A vector space over a division ring $D$ is by definition a unitary module over $D$. 
$S$ is a division ring by assumption.
$\struct {R, +, \circ_S}_S$ is a unitary module by Subring Module is Module/Special Case.
{{qed}}
Theorem: Vector Space on Field Extension is Vector Space

Let $\struct {K, +, \times}$ be a field.
Let $L / K$ be a field extension over $K$.
Let $\struct {L, +, \times}_K$ be the a vector space of $L$ over $K$.
Then $\struct {L, +, \times}_K$ is a vector space.

Proof:
By definition, $L / K$ is a field extension over $K$.
Thus, by definition, $K$ is a subfield of $L$.
Thus, also by definition, $K$ is a division subring of $L$.
The result follows by Vector Space over Division Subring is Vector Space.
{{qed}}
Category:Examples of Vector Spaces
hv8bgifu71tkrwb1ltfyu52uhx2gdy4
Theorem: Condition for Linear Divisor of Polynomial

Let $\map P x$ be a polynomial in $x$.
Let $a$ be a constant.
Then $x - a$ is a divisor of $\map P x$ {{iff}} $a$ is a root of $P$.

Proof:
From the Little Bézout Theorem, the remainder of $\map P x$ when divided by $x - a$ is equal to $\map P a$.
Theorem: Complex Number is Algebraic over Real Numbers

Let $z \in \C$ be a complex number.
Then $z$ is algebraic over $\R$.

Proof:
Let $z = a + i b$.
Let $\overline z = a - i b$ be the complex conjugate of $z$.
From Product of Complex Number with Conjugate:
:$z \overline z = a^2 + b^2$
From Sum of Complex Number with Conjugate:
:$z + \overline z = 2 a$
Thus from Viète's Formulas, both $z$ and $\overline z$ are roots of the polynomial:
:$X^2 - 2 a X + \paren {a^2 + b^2}$
Hence the result by definition of algebraic over $\R$.
{{qed}}
Theorem: Polynomial with Algebraic Number as Root is Multiple of Minimal Polynomial

Let $F$ be a field.
Let $\map P x$ be a polynomial in $F$.
Let $z$ be a root of $\map P x$.
Then $\map P x$ is a multiple of the minimal polynomial $\map m x$ in $z$ over $F$.

Proof:
For $z$ to be a root of $F$, $z$ must be algebraic over $F$.
Let us write:
:$\map P x = \map m x \, \map q x + \map r x$
where $\map q x$ and $\map r x$ are polynomials in $F$.
Then either $\map r x = 0$ or $\map \deg {\map r x} < \map \deg {\map m x}$.
Then:
:$\map P z = \map m z \, \map q z + \map r z$
But as $z$ is a root of both $\map P x$ and $\map m x$, we have that:
:$\map P z = \map m z = 0$
and so:
:$\map r z = 0$
So if $\map r x \ne 0$ we have that $\map r x$ is a polynomial of smaller degree than $\map m x$.
This contradicts the minimality of $\map m x$.
Thus $\map r x = 0$ and so $\map P x$ is a multiple of $\map m x$.
{{qed}}
Theorem: Simple Algebraic Field Extension consists of Polynomials in Algebraic Number

Let $F$ be a field.
Let $\theta \in \C$ be algebraic over $F$.
Let $\map F \theta$ be the simple field extension of $F$ by $\theta$.
Then $\map F \theta$ consists of polynomials that can be written in the form $\map f \theta$, where $\map f x$ is a polynomial over $F$.

Proof:
Let $H$ be the set of all numbers which can be written in the form $\map f \theta$.
We have that:
:$H$ is closed under addition and multiplication.
:$H$ contains $0$ and $1$
:For every element of $H$, $H$ also contains its negative.
Let $\map f \theta \ne 0$.
Then $\theta$ is not a root of $\map f x$.
Hence from Polynomial with Algebraic Number as Root is Multiple of Minimal Polynomial:
:the minimal polynomial $\map m x$ in $\theta$ does not divide $\map f x$.
From Minimal Polynomial is Irreducible, the GCD of $\map m x$ and $\map f x$ is $1$.
Therefore:
:$\exists \map s x, \map t x: \map s x \map m x + \map t x \map f x = 1$
Substituting for $\theta$:
:$\map s \theta \, \map m \theta + \map t \theta \, \map f \theta = 1$
Because $\map m \theta = 0$ it follows that:
:$\map t \theta \, \map f \theta = 1$
We have that $\map t \theta \in H$.
Thus $\map t \theta$ is the product inverse of $\map f x$ in $H$.
Thus $H$ is a field.
A field containing $F$ and $\theta$ must contain $1$ and all the powers of $\theta$ for positive integer index.
Hence such a field also contains all linear combinations of these, with coefficients in $F$.
So a field containing $F$ and $\theta$ contains all the elements of $H$:
:$H \subseteq \map F \theta$
But by definition, $\map F \theta$ is the smallest field containing $F$ and $\theta$.
That is:
:$\map F \theta \subseteq H$
Thus:
:$\map F \theta = H$
and the result follows.
{{Qed}}
Theorem: Element of Simple Algebraic Field Extension of Degree n is Polynomial in Algebraic Number of Degree Less than n

Let $F$ be a field.
Let $\theta \in \C$ be algebraic over $F$ of degree $n$.
Let $\map F \theta$ be the simple field extension of $F$ by $\theta$.
Then any element of $\map F \theta$ can be written as $\map f \theta$, where $\map f x$ is a polynomial over $F$ of degree at most $n - 1$.

Proof:
From Simple Algebraic Field Extension consists of Polynomials in Algebraic Number, an arbitrary element of $\map F \theta$ can be written as $\map f \theta$.
But:
:$\map f x = \map m x \, \map q x + \map r x$
where:
:$\map m x$ is minimal polynomial in $\theta$
:$\map q x$ is a polynomial in $\map F \theta$
:$\map r x$ is a polynomial in $\map F \theta$ such that either:
::$\map \deg {\map r x} < \map \deg {\map m x}$
:or:
::$\map r x = 0$
Thus:
:$\map f \theta = \map m \theta \, \map q \theta + \map r \theta$
and as $\map m \theta = 0$ we have:
:$\map f \theta = \map r \theta$
So $\map f \theta$ can be expressed as $\map r \theta$ instead, which is of degree strictly less than that of $\map m \theta$.
Hence the result.
{{Qed}}
Theorem: Degree of Simple Algebraic Field Extension equals Degree of Algebraic Number

Let $F$ be a field.
Let $\theta \in \C$ be algebraic over $F$ of degree $n$.
Let $\map F \theta$ be the simple field extension of $F$ by $\theta$.
Then $\map F \theta$ is a finite extension of $F$ whose degree is:
:$\index {\map F \theta} F = n$

Proof:
Considered as a vector space over $F$, $\map F \theta$ is generated by the set $B$, where:
:$B := \set {1, \theta, \theta^2, \ldots, \theta^{n - 1} }$
But $S$ is linearly independent over $F$, because otherwise:
:$c_0 1 + c_1 \theta + c_2 \theta^2 + \dotsb + c_{n - 1} \theta^{n - 1} = 0$
with all the $c$s non-zero.
That would mean $\theta$ was the root of a polynomial whose degree was less than that of the minimal polynomial $\map m x$ of $\theta$, whose degree equals $n$.
Therefore $B$ is a basis of $\map F \theta$ over $F$.
Thus $\map F \theta$ is of dimension $\size B = n$.
Hence the $\index {\map F \theta} F = n$.
{{Qed}}
Theorem: Degree of Element of Finite Field Extension divides Degree of Extension

Let $F$ be a field whose zero is $0$ and whose unity is $1$.
Let $K / F$ be a finite field extension of degree $n$.
Let $\alpha \in K$ be algebraic over $F$.
Then the degree of $\alpha$ is a divisor of $n$.

Proof:
Let $\alpha \in K$.
The dimension of $K / F$ considered as a vector space is $n$.
Let $S$ be the set defined as:
:$S := \set {1, \alpha, \alpha^2, \ldots, \alpha_n}$
We have that:
:$\card S = n + 1$
From Cardinality of Linearly Independent Set is No Greater than Dimension:
:$S$ is linearly dependent on $F$.
Hence there are scalars $c_0, c_1, \ldots, c_n \in F$, not all zero, such that:
:$c_0 + c_1 \alpha + c_2 \alpha^2 + \dotsb + c_n \alpha_n = 0$
which is a polynomial of degree $n$.
So $\alpha$ is algebraic over $F$ with degree no greater than $n$.
Consider $\map F \alpha$, the simple algebraic extension of $F$ on $\alpha$.
We have that:
:$F \subseteq \map F \alpha \subseteq K$
Let $\alpha$ be algebraic over $F$ with degree $m$.
Then $\map F \alpha$ is a finite extension of $F$ with degree $\index {\map F \alpha} F = m$.
We also have that $K$ is a finite extension of $F$ with degree $n$.
So by Degree of Field Extensions is Multiplicative:
:$\index K F = \index K {\map F \alpha} \index {\map F \alpha} F$
But $\index K F = n$ and $\index {\map F \alpha} F = m$
so it follows that:
:$m \divides n$
The result follows.
{{Qed}}
Theorem: Algebraic Element of Degree 3 is not Element of Field Extension of Degree Power of 2

Let $K / F$ be a finite field extension of degree $2^m$.
Let $\alpha \in K$ be algebraic over $F$ with degree $3$.
Then $\alpha \notin K$.

Proof:
{{AimForCont}} $\alpha \in K$.
From Degree of Element of Finite Field Extension divides Degree of Extension:
:$\map \deg \alpha \divides \map \deg {K / F}$
But:
:$3 \nmid 2^m$
From this contradiction, it follows that $\alpha \notin K$.
{{qed}}
Theorem: Construction of Point in Cartesian Plane with Rational Coordinates

Let $\CC$ be a Cartesian plane.
Let $P = \tuple {x, y}$ be a rational point in $\CC$.
Then $P$ is constructible using a compass and straightedge construction.

Proof:
Let $x = \dfrac m n$ where $m, n \in \Z_{\ne 0}$ are non-zero integers.
Let $y = \dfrac r s$ where $r, s \in \Z_{\ne 0}$ are non-zero integers.
Let $O$ denote the point $\tuple {0, 0}$.
Let $A$ denote the point $\tuple {1, 0}$.
Let $M$ denote the point $\tuple {0, m}$.
Let $N$ denote the point $\tuple {0, n}$.
The $x$-axis is identified with the straight line through $O$ and $A$.
The $y$-axis is constructed as the line perpendicular to $OA$ through $O$.
Using Construction of Lattice Point in Cartesian Plane, the points $M$ and $N$ are constructed.
The line $NA$ is drawn.
Using Construction of Parallel Line, $MQ$ is drawn, where $Q$ is the point of intersection of $MQ$ with the $x$-axis.
We have that $\dfrac {OM} {ON} = \dfrac m n$
As $\triangle ONA$ is similar to $\triangle OMQ$, it follows that $\dfrac {OM} {ON} = \dfrac {OQ} {OA}$
Therefore $Q$ is the point $\tuple {\dfrac m n, 0}$.
:400px
Let $y = \dfrac r s$ where $r, s \in \Z_{\ne 0}$ are non-zero integers.
Using Construction of Lattice Point in Cartesian Plane, the points $\tuple {r, 0}$ and $\tuple {s, 0}$ are constructed.
Using the same technique as above, {{mutatis}}, the point $\tuple {0, \dfrac r s}$ is constructed.
Using Construction of Parallel Line, a straight line is drawn through $\tuple {\dfrac m n, 0}$ parallel to the $y$-axis.
Using Construction of Parallel Line, a straight line is drawn through $\tuple {0, \dfrac r s}$ parallel to the $x$-axis.
By definition of Cartesian plane, their intersection is at $\tuple {\dfrac m n, \dfrac r s}$, which is the required point $P = \tuple {x, y}$.
{{qed}}
Theorem: Construction of Integer Multiple of Line Segment

Let $AB$ be a line segment in the plane.
Let $AC$ be a line segment in the plane through a point $C$
Let $D$ be a point on $AC$ such that $AD = n AB$ for some $n \in \Z$.
Then $AD$ is constructible using a compass and straightedge construction.

Proof:
Let $AB$ be given.
Let the straight line through $AC$ be constructed.
Let $D_1$ be constructed on $AC$ such that $A D_1 = AB$ by constructing a circle whose center is at $A$ and whose radius is $B$.
Let $D_0$ be identified as the point $A$.
For each $k \in \set {1, 2, \ldots, n - 1}$, construct a circle whose center is at $D_k$ and whose radius is $D_{k - 1} D_k$.
We have that $D_k D_{k + 1} = D_{k - 1} D_k = AB$.
Thus $D_0 D_{k + 1}$ is ${k + 1}$ times $D_0 D_1 = AB$.
When $k = n - 1$ we have that $D_{k + 1} = D_n = D$ is $n$ times $AB$.
The diagram below illustrates the construction for $n = 4$.
:800px
{{qed}}
Category:Euclidean Geometry
Category:Compass and Straightedge Constructions
344wpkd00u9lftfiqpo62uot0oos2gx
Theorem: Point in Plane is Constructible iff Coordinates in Extension of Degree Power of 2

Let $\CC$ be a Cartesian plane.
Let $S$ be a set of points in $\CC$.
Let $F$ be the smallest field containing all the coordinates of the points in $S$.
Let $P = \tuple {a, b}$ be a point in $\CC$.
Then:
:$P$ is constructible from $S$ using a compass and straightedge construction
{{iff}}:
:the coordinates of $P$ are contained in a finite extension $K$ of $F$ whose degree is given by:
::$\index K F = 2^m$
:for some $m \in \Z_{\ge 0}$.

Proof:
A point $P$ is constructed in a compass and straightedge construction from one of $3$ basic operations:
:$(1): \quad$ the intersection of $2$ straight lines
:$(2): \quad$ the intersection of a straight line and the circumference of a circle
:$(3): \quad$ the intersection of the circumferences of $2$ circle.
Let $A$, $B$, $C$ and $D$ be points in $S$.
In case $(1)$, the equations defining the straight lines $AB$ and $CD$ are polynomials of degree $1$.
Hence the coordinates of $P$ can be found by solving the linear simultaneous equations defining $AB$ and $CD$.
It follows that the solution is in $F$.
{{qed|lemma}}
In case $(2)$:
:the equation defining the circle whose center is at $A$ and whose radius is $AB$ is of the form $x^2 + y^2 + 2 f x + 2 g y + c = 0$, where $c, f, g \in F$.
while:
:the equation defining the straight line $CD$ is a polynomial of degree $1$.
The $x$-coordinate of $P$ is then the root of a quadratic equation with coefficients in $F$.
The $y$-coordinate of $P$ is then found by solving a linear equation.
Thus the coordinates of $P$ are elements of either a field extension of $F$ of degree $2$ or of $F$ itself.
In case $(3)$:
:the equation defining the circle whose center is at $A$ and whose radius is $AB$ is of the form $x^2 + y^2 + 2 f x + 2 g y + c = 0$, where $c, f, g \in F$
:the equation defining the circle whose center is at $C$ and whose radius is $CD$ is of the form $x^2 + y^2 + 2 f' x + 2 g' y + c' = 0$, where $c', f', g' \in F$.
The solution of these equations is the same as the solution of either circle and the straight line $2 \paren {f - f'} x + 2 \paren {g - g'} y + \paren {c - c'} = 0$, which is the same as case $(2)$.
We have that the coordinates of the various points belong to the field $F = F_0$, say.
Suppose $P$ is constructed using $k$ of the basic constructions $(1)$, $(2)$ and $(3)$.
Let $F_i$ be the smallest field containing all the points so far obtained by $i$ such constructions, for $i = 1, 2, \ldots, k$.
Either $F_i = F_{i - 1}$ or $F_i$ is an finite extension of $F_i$ of degree $2$.
Thus for each $i$, either:
:$\index {F_i} {F_{i - 1} } = 1$
or:
:$\index {F_i} {F_{i - 1} } = 2$
Therefore:
:$\index {F_k} {F_0} = \index {F_k} {F_{k - 1} } \index {F_{k - 1} } {F_{k - 2} } \dotsm  {F_1} {F_0} = 2^m$
where $0 \le m \le k$.
Hence the result.
{{qed}}