avewright/proofwiki-math huggingface dataset:
Theorem: Conditional is Left Distributive over Conjunction

The implication operator is left distributive over the conjunction operator:
=== Formulation 1 ===
{{:Conditional is Left Distributive over Conjunction/Formulation 1}}
=== Formulation 2 ===
{{:Conditional is Left Distributive over Conjunction/Formulation 2}}

Proof:
Let us use the following abbreviations
{{begin-eqn}}
{{eqn | l = \phi
      | o = \text {for}
      | r = \paren {p \implies q} \land \paren {p \implies r}
      | c = 
}}
{{eqn | l = \psi
      | o = \text {for}
      | r = p \implies \paren {q \land r}
      | c = 
}}
{{end-eqn}}
{{BeginTableau|\vdash \phi \implies \psi}}
{{Assumption|1|\phi}}
{{SequentIntro|2|1|\psi|1|Conditional is Left Distributive over Conjunction: Formulation 1}}
{{Implication|3||\phi \implies \psi|1|2}}
{{EndTableau}}
Expanding the abbreviations leads us back to:
:$\paren {\paren {p \implies q} \land \paren {p \implies r} } \implies \paren {p \implies \paren {q \land r} }$
{{qed}}
Theorem: Existence of Negation Normal Form of Statement

Any propositional formula can be expressed in negation normal form (NNF).

Proof:
A propositional variable is already trivially in negation normal form (NNF).
So we consider the general propositional formula $S$.
In the following, $P$ and $Q$ are to stand for general propositional formulas.
First, from Functionally Complete Logical Connectives: Conjunction, Negation and Disjunction we have that:
:$\set {\neg, \land, \lor}$
forms a functionally complete set of logical connectives.
So we can convert $S$ so that:
:by the definition of the biconditional, instances of $P \iff Q$ can be converted into $\paren {P \implies Q} \land \paren {Q \implies P}$
:by the Rule of Material Implication, instances of $P \implies Q$ can be converted into $\neg P \lor Q$.
Other connectives can likewise be treated appropriately.
Thus $S$ will contain nothing but connectives from $\set {\neg, \land, \lor}$.
Next we can replace:
:instances of $\neg \paren {P \land Q}$ with $\neg P \lor \neg Q$, by De Morgan's Laws: Disjunction of Negations
:instances of $\neg \paren {P \lor Q}$ with $\neg P \land \neg Q$, by De Morgan's Laws: Conjunction of Negations
:instances of $\neg \neg P$ with $P$ by Double Negation Elimination.
At any stage where a negation appears before a parenthesis, it will then appear before the statements inside the parenthesis.
Thus the negation signs gradually move inwards or are eliminated.
Eventually all remaining negation signs will appear next to simple statements.
Hence the result.
{{qed}}
Category:Negation Normal Form
blr188m637eexy94n7bf6xpbvraxht4
Theorem: Existence of Conjunctive Normal Form of Statement

Any propositional formula can be expressed in conjunctive normal form (CNF).

Proof:
A propositional variable is already trivially in conjunctive normal form (CNF).
So we consider the general propositional formula $S$.
First we convert to negation normal form (NNF).
This is always possible, by Existence of Negation Normal Form of Statement.
Now $S$ will be of the form:
:$P_1 \land P_2 \land \cdots \land P_n$
where $P_1, P_2, \ldots, P_n$ are either:
:literals
or:
:statements of the form $\paren {Q_1 \lor Q_2 \lor \ldots \lor Q_n}$.
If all the $Q_1, \ldots, Q_n$ are literals we have finished.
Otherwise they will be of the form:
:$Q_j = \paren {R_1 \land R_2 \land \ldots \land R_m}$
If the latter is the case, then use the Disjunction Distributes over Conjunction to convert:
:$Q_1 \lor Q_2 \lor \ldots \lor \paren {R_1 \land R_2 \land \ldots \land R_m} \ldots \lor Q_n$
into:
{{begin-eqn}}
{{eqn | o = 
      | r = \paren {Q_1 \lor Q_2 \lor \ldots \lor Q_n \lor R_1}
      | c = 
}}
{{eqn | o = \land
      | r = \paren {Q_1 \lor Q_2 \lor \ldots \lor Q_n \lor R_2}
      | c = 
}}
{{eqn | o = \land
      | r = \ldots
      | c = 
}}
{{eqn | o = \land
      | r = \paren {Q_1 \lor Q_2 \lor \ldots \lor Q_n \lor R_m}
      | c = 
}}
{{end-eqn}}
It is taken for granted that Disjunction is Associative and Disjunction is Commutative.
It can be seen then that each of the
:$\paren {Q_1 \lor Q_2 \lor \ldots \lor Q_n \lor R_k}$
are terms in the CNF expression required.
If any terms are still not in the correct format, then use the above operation until they are.
{{qed}}
Theorem: Existence of Disjunctive Normal Form of Statement

Any propositional formula can be expressed in disjunctive normal form (DNF).

Proof:
A propositional variable is already trivially in disjunctive normal form (DNF).
So we consider the general propositional formula $S$.
First we convert to negation normal form (NNF).
This is always possible, by Existence of Negation Normal Form of Statement.
Now $S$ will be of the form:
:$P_1 \lor P_2 \lor \cdots \lor P_n$
where $P_1, P_2, \ldots, P_n$ are either:
:literals
or:
:statements of the form $\paren {Q_1 \land Q_2 \land \ldots \land Q_n}$
If all the $Q_1, \ldots, Q_n$ are literals we have finished.
Otherwise they will be of the form $Q_j = \paren {R_1 \lor R_2 \lor \ldots \lor R_m}$
If the latter is the case, then use Conjunction Distributes over Disjunction to convert:
:$Q_1 \land Q_2 \land \ldots \land \paren {R_1 \lor R_2 \lor \ldots \lor R_m} \ldots \land Q_n$
into:
{{begin-eqn}}
{{eqn | o = 
      | r = \paren {Q_1 \land Q_2 \land \ldots \land Q_n \land R_1}
      | c = 
}}
{{eqn | o = \lor
      | r = \paren {Q_1 \land Q_2 \land \ldots \land Q_n \land R_2}
      | c = 
}}
{{eqn | o = \lor
      | r = \ldots
      | c = 
}}
{{eqn | o = \lor
      | r = \paren {Q_1 \land Q_2 \land \ldots \land Q_n \land R_m}
      | c = 
}}
{{end-eqn}}
It is taken for granted that Conjunction is Associative and Conjunction is Commutative.
It can be seen then that each of the
:$\paren {Q_1 \land Q_2 \land \ldots \land Q_n \land R_k}$
are terms in the DNF expression required.
If any terms are still not in the correct format, then use the above operation until they are.
{{qed}}
Theorem: Existence of Base-N Representation

{{refactor|lemmata and sub proofs|level = medium}}
{{tidy|Could be improved in presentational style}}
Given a number $x \in \hointr 0 1$, there exists a representation of that number in a base-$p$ positional system.
Specifically, there exists a sequence $\sequence {a_n}$ such that:
:$0 \le a_n < p$, and
:$\ds \sum_{n \mathop = 1}^\infty \frac {a_n} {p^n}$ converges to $x$.
Unless $\sequence {a_n}$ terminates (that is $a_n = 0$ for all sufficiently large $n$), then this representation is unique.
If $\sequence {a_n}$ does terminate, then there is exactly one other sequence which satisfies the criteria of the theorem.

Proof:
=== Existence of Representation === 
Define:
:$\ds a_j = \floor {\paren {x - \sum_{i \mathop = 1}^{j - 1} \frac {a_i} {p^i} } p^j}$
where we accept the vacuous summation $\ds \sum_{i \mathop = 1}^0 a_i p^{-i} = 0$.
This recursive definition allows for all $a_n$ to be computed.
Theorem: Symmetry Group of Equilateral Triangle is Group

The symmetry group of the equilateral triangle is a group.

Proof:
Let us refer to this group as $D_3$.
Taking the group axioms in turn:
Theorem: Order of General Linear Group over Galois Field

Let $\GF$ be a Galois field with $p$ elements.
Then the order of the general linear group $\GL {n, \GF}$ is:
:$\ds \prod_{j \mathop = 1}^n \paren {p^n - p^{j - 1} }$

Proof:
Let $\GF$ be a Galois field with $p$ elements: $\card \GF = p$.
Let $A = \sqbrk {a_{i j} }_{n, n}$ be a matrix such that $\size A \ne 0$ and $a_{i j} \in \GF$.
How many such matrices can be constructed?
In order to avoid a zero determinant, the top row of the matrix, $\sequence {a_{1 j} }_{j \mathop = 1, \dotsc, n}$ must have at least one non-zero element.
Therefore there are $p^n - 1$ possibilities for the top row:
:the $p^n$ possible sequences of $n$ values from $\GF$, minus the one sequence $\paren {0, 0, \dotsc, 0}$.
The only restriction on the second row is that it not be a multiple of the first.
Therefore, there are the $p^n$ possible sequences again, minus the $p$ sequences which are multiples of the first row.
Thus, continuing in this fashion, the $j^{th}$ row can be any of the $p^n$ possible sequences, minus the $p^{\paren {j - 1} }$ sequences which are linear combinations of previous rows.
The number of possible matrices satisfying the conditions of $A$, then, is:
:$\ds \prod_{j \mathop = 1}^n \paren {p^n - p^{j - 1} }$
{{qed}}
Category:Combinatorics
Category:General Linear Group
Category:Galois Fields
ca1boiomzifyos0ekvcnzyzp3o67tpe
Theorem: Existence of Latin Squares

For each $n \in \Z_{>0}$ there exists at least one Latin square of order $n$.

Proof:
The Cayley table of a finite group of order $n$ is a Latin square, from Group has Latin Square Property.
For every $n \in \Z_{>0}$ there exists a cyclic group of order $n$.
It follows that for every $n \in \Z_{>0}$ the Cayley table of the cyclic group of order $n$ is a Latin square of order $n$.
{{qed}}
Category:Latin Squares
lcrxk2uq9h858urmw4nuqubls67htzj
Theorem: Hilbert's Basis Theorem

Let $A$ be a Noetherian ring.
Let $A \sqbrk x$ be the ring of polynomial forms over $A$ in the single indeterminate $x$.
Then $A \sqbrk x$ is also a Noetherian ring.

Proof:
From the definition, a Noetherian ring is also a commutative ring with unity.
Let $f = a_n x^n + \cdots + a_1 x + a_0 \in A \sqbrk x$ be a polynomial over $x$.
Let $I \subseteq A \sqbrk x$ be an ideal of $A \sqbrk x$.
We will show that $I$ is finitely generated. 
Let $f_1$ be an element of least degree in $I$, and let $\ideal {g_1, \ldots, g_r}$ denote the ideal generated by the polynomials $g_1, \dotsc, g_r$.
For $i \ge 1$, if $\ideal {f_1, \ldots, f_i} \ne I$, then choose $f_{i + 1}$ to be an element of minimal degree in $I \setminus \ideal {f_1, \ldots, f_i}$.
If $\ideal {f_1, \ldots, f_i} = I$ then stop choosing elements.
Let $a_j$ be the leading coefficient of $f_j$.
Since $A$ is Noetherian, the ideal $\ideal {a_1, a_2, \ldots} \subseteq A$ is generated by $a_1, a_2, \ldots, a_m$ for some $m \in \N$.
We claim that $f_1, f_2, \ldots, f_m$ generate $I$.
{{AimForCont}} not.
Then our process chose an element $f_{m + 1}$, and $\ds a_{m + 1} = \sum_{j \mathop = 1}^m u_j a_j$ for some $u_j \in A$.
Since the degree of $f_{m + 1}$ is greater than or equal to the degree of $f_j$ for $j = 1, \ldots, m$, the polynomial:
:$\ds g = \sum_{j \mathop = 1}^m u_j f_j x^{\deg f_{m + 1} - \deg f_j} \in \ideal {f_1, \ldots, f_m}$
has the same leading coefficient and degree as $f_{m + 1}$.
The difference $f_{m + 1} - g$ is not in $\ideal {f_1, \ldots, f_m}$ and has degree strictly less than $f_{m + 1}$, a contradiction of our choice of $f_{m + 1}$.
Thus $I = \ideal {f_1, \ldots, f_m}$ is finitely generated, and the proof is complete.
{{qed}}
{{Namedfor|David Hilbert|cat = Hilbert}}
Category:Noetherian Rings
Category:Commutative Algebra
cs4wcmxe1vkplfi3357w1k3i055rksk
Theorem: Lipschitz Condition implies Uniform Continuity

Let $\struct {M_1, d_1}$ and $\struct {M_2, d_2}$ be metric spaces.
Let $g: M_1 \to M_2$ satisfy the Lipschitz condition.
Then $g$ is uniformly continuous on $M_1$.

Proof:
Let $\epsilon > 0$, $x,y \in M_1$. 
Let $K$ be a Lipschitz constant for $g$.
First, suppose that $K \le 0$.
Then:
:$\map {d_1} {x, y} \le 0 \map {d_2} {\map g x, \map g y}$ by the Lipschitz condition on $g$.
So $\map {d_1} {x, y} \le 0 \implies \map {d_1} {x, y} = 0 \implies x = y$ for all $x$ and $y$ in $M_1$.
Thus $g$ is a constant function, which is uniformly continuous.
Next, suppose that $K > 0$.
Take $\delta = \epsilon / K$.
Then if $\map {d_1} {x, y} < \delta$, we have:
:$K \map {d_1} {x, y} < \epsilon$
By the Lipschitz condition on $g$, we know that:
:$\map {d_2} {\map g x, \map g  y} \le K \map {d_1} {x, y}$
These last two statements together imply $\map {d_2} {\map g x, \map g y} < \epsilon$.
Thus, $g$ is uniformly continuous on $M_1$.
{{qed}}
Category:Metric Spaces
Category:Uniformly Continuous Mappings
l37toybgo8xw36lmwkv7c5pv2aa8hoc
Theorem: Existence of Cyclic Group of Order n

Let $n \in \Z_{>0}$.
Then there exists a cyclic group of order $n$ which is unique up to isomorphism.

Proof:
Existence follows from Integers Modulo m under Addition form Cyclic Group.
Uniqueness follows from Cyclic Groups of Same Order are Isomorphic.
{{Qed}}
Theorem: Quotient Group is Group

Let $G$ be a group.
Let $N$ be a normal subgroup of $G$.
Then the quotient group $G / N$ is indeed a group.

Proof:
By Subgroup is Normal iff Left Cosets are Right Cosets, the set of left cosets for $N$ equals the set of right cosets.
It follows that $G / N$ does not depend on whether left cosets are used to define it or right cosets.
{{WLOG}}, we will work with the left cosets.
By definition of quotient group, the elements of $G / N$ are the cosets of $N$ in $G$, where the group operation is defined as:
:$\paren {a N} \paren {b N} = \paren {a b} N$
The operation has been shown in Coset Product is Well-Defined to be a well-defined operation.
Now we need to demonstrate that $G / N$ is a group.
Theorem: Principal Ideal is Ideal

Let $\struct {R, +, \circ}$ be a ring with unity.
Let $a \in R$.
Let $\ideal a$ be the principal ideal of $R$ generated by $a$.
Then $\ideal a$ is an ideal of $R$.

Proof:
First we establish that $\ideal a$ is an ideal of $R$, by verifying the conditions of Test for Ideal.
$\ideal a \ne \O$, as $1_R \circ a = a \in \ideal a$.
Let $x, y \in \ideal a$.
Then:
{{begin-eqn}}
{{eqn | q = \exists r, s \in R
      | l = x
      | r = r \circ a, y = s \circ a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x + \paren {-y}
      | r = r \circ a + \paren {-s \circ a}
      | c = 
}}
{{eqn | r = \paren {r + \paren {-s} } \circ a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x + \paren {-y}
      | o = \in
      | r = \ideal a
      | c = 
}}
{{end-eqn}}
Let $s \in \ideal a, x \in R$.
{{begin-eqn}}
{{eqn | l = s
      | o = \in
      | r = \ideal a, x \in R
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists r \in R
      | l = s
      | r = r \circ a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x \circ s
      | r = x \circ r \circ a
      | c = 
}}
{{eqn | o = \in
      | r = \ideal a
      | c = 
}}
{{end-eqn}}
and similarly $s \circ x \in \ideal a$.
Thus by Test for Ideal, $\ideal a$ is an ideal of $R$.
{{qed}}
Theorem: Bézout's Theorem

Let $X$ and $Y$ be two plane projective curves defined over a field $F$ that do not have a common component.
Then the total number of intersection points of $X$ and $Y$ with coordinates in an algebraically closed field $E$ which contains $F$, counted with their multiplicities, is equal to the product of the degrees of $X$ and $Y$.

Proof:
The condition that $X$ and $Y$ have no common component is true if both $X$ and $Y$ are defined by different irreducible polynomials.
In particular, it holds for a pair of "generic" curves.
{{ExtractTheorem|Link to a proof of the above}}
{{ProofWanted}}
Theorem: Forward Difference of Power

:$\Delta c^x = \paren {c - 1} c^x$
where $\Delta$ denotes the forward difference operator.

Proof:
From the definitions:
{{begin-eqn}}
{{eqn | l = \Delta c^x
      | r = c^{x + 1} - c^x
      | c = {{Defof|Forward Difference Operator}}
}}
{{eqn | r = c \cdot c^x - c^x
}}
{{eqn | r = \paren {c - 1} c^x
}}
{{end-eqn}}
{{qed}}
Category:Finite Calculus
m0tf2vwc49nhv5xfxhzhmznqqd9sidk
Theorem: Forward Difference of Harmonic Number Function

Let $H_x$ denote the harmonic number function.
Then:
:$\Delta H_x = \dfrac 1 {x + 1}$
where $\Delta H_x$ denotes the forward difference operator.

Proof:
From the definitions:
{{begin-eqn}}
{{eqn | l = \Delta H_x
      | r = H_{x + 1} - H_x
      | c = {{Defof|Forward Difference Operator}}
}}
{{eqn | r = \sum_{k \mathop = 1}^{x + 1} \frac 1 k - \sum_{k \mathop = 1}^x \frac 1 k
      | c = {{Defof|Harmonic Number}}
}}
{{eqn | r = \sum_{k \mathop = 1}^x \frac 1 k + \frac 1 {x + 1} - \sum_{k \mathop = 1}^x \frac 1 k
}}
{{eqn | r = \frac 1 {x + 1}
}}
{{end-eqn}}
{{qed}}
Category:Finite Calculus
Category:Harmonic Numbers
a1hk7ogvsn85vwdmh4j60qpany0nqzi
Theorem: Equality of Ordered Tuples

Let $a = \tuple {a_1, a_2, \ldots, a_n}$ and $b = \tuple {b_1, b_2, \ldots, b_n}$ be ordered tuples.
Then:
:$a = b \iff \forall i: 1 \le i \le n: a_i = b_i$
That is, for two ordered tuples to be equal, all the corresponding elements have to be equal.

Proof:
Proof by induction:
For all $n \in \N_{>0}$, let $\map P n$ be the proposition:
:$\tuple {a_1, a_2, \ldots, a_n} = \tuple {b_1, b_2, \ldots, b_n} \iff \forall i: 1 \le i \le n: a_i = b_i$
$\map P 1$ is true, as this just says $\tuple {a_1} = \tuple {b_1} \iff a_1 = b_1$ which is trivial.
Theorem: Zero of Power Set with Union

Let $S$ be a set and let $\powerset S$ be its power set.
Consider the algebraic structure $\struct {\powerset S, \cup}$, where $\cup$ denotes set union.
Then $S$ serves as the zero element for $\struct {\powerset S, \cup}$.

Proof:
We note that by Set is Subset of Itself, $S \subseteq S$ and so $S \in \powerset S$ from the definition of the power set.
From Union with Superset is Superset, we have:
:$A \subseteq S \iff A \cup S = S = S \cup A$.
By definition of power set:
:$A \subseteq S \iff A \in \powerset S$
So:
:$\forall A \in \powerset S: A \cup S = S = S \cup A$
Thus we see that $S$ acts as the zero.
{{qed}}
Theorem: Zero of Power Set with Intersection

Let $S$ be a set and let $\powerset S$ be its power set.
Consider the algebraic structure $\struct {\powerset S, \cap}$, where $\cap$ denotes set intersection.
Then the empty set $\O$ serves as the zero element for $\struct {\powerset S, \cap}$.

Proof:
From Empty Set is Element of Power Set:
:$\O \in \powerset S$
From Intersection with Empty Set:
:$\forall A \subseteq S: A \cap \O = \O = \O \cap A$
By definition of power set:
:$A \subseteq S \iff A \in \powerset S$
So:
:$\forall A \in \powerset S: A \cap \O = \O = \O \cap A$
Thus we see that $\O$ acts as the zero element for $\struct {\powerset S, \cap}$.
{{qed}}
Theorem: Strictly Positive Real Numbers under Multiplication form Uncountable Abelian Group

Let $\R_{>0}$ be the set of strictly positive real numbers:
:$\R_{>0} = \set {x \in \R: x > 0}$
The structure $\struct {\R_{>0}, \times}$ is an uncountable abelian group.

Proof:
From Strictly Positive Real Numbers under Multiplication form Subgroup of Non-Zero Real Numbers we have that $\struct {\R_{>0}, \times}$ is a subgroup of $\struct {\R_{\ne 0}, \times}$, where $\R_{\ne 0}$ is the set of real numbers without zero:
:$\R_{\ne 0} = \R \setminus \set 0$
From Subgroup of Abelian Group is Abelian it also follows that $\struct {\R_{>0}, \times}$ is an abelian group.
Its infinite nature follows from the nature of real numbers.
{{Handwaving|Strictly state how the positive real numbers are uncountable. Straightforward, but we have no page for it.}}
{{qed}}
Theorem: One-Parameter Family of Curves for First Order ODE

Every one-parameter family of curves is the general solution of some first order ordinary differential equation.
Conversely, every first order ordinary differential equation has as its general solution some one-parameter family of curves.

Proof:
From Picard's Existence Theorem, every point in a given rectangle is passed through by some curve which is the solution of a given integral curve of a differential equation.
The equation of this family can be written as:
:$y = \map y {x, c}$
where different values of $c$ give different curves.
The integral curve which passes through $\tuple {x_0, y_0}$ corresponds to the value of $c$ such that:
:$y_0 = \map y {x_0, c}$
Conversely, consider the one-parameter family of curves described by:
:$\map f {x, y, c} = 0$
Differentiate $f$ {{WRT|Differentiation}} $x$ to get a relation in the form:
:$\map g {x, y, \dfrac {\d y} {\d x}, c} = 0$
Then eliminate $c$ between these expressions for $f$ and $g$ and get:
:$\map F {x, y, \dfrac {\d y} {\d x} } = 0$
which is a first order ordinary differential equation.
{{qed}}
Theorem: Orthogonal Trajectories of One-Parameter Family of Curves

Every one-parameter family of curves has a unique family of orthogonal trajectories.

Proof:
Let $\map f {x, y, z}$ define a one-parameter family of curves $\FF$.
From One-Parameter Family of Curves for First Order ODE, there is a corresponding first order ODE:
:$\map F {x, y, \dfrac {\d y} {\d x} }$
whose solution is $\FF$.
From Slope of Orthogonal Curves, the slope of one curve is the negative reciprocal of any curve orthogonal to it.
So take the equation:
:$\map F {x, y, \dfrac {\d y} {\d x} }$
and from it create the equation:
:$\map F {x, y, -\dfrac {\d x} {\d y} }$
that is, replace $\dfrac {\d y} {\d x}$ with $-\dfrac {\d x} {\d y}$.
This is also a first order ODE, which corresponds with a one-parameter family of curves $\GG$ defined by the implicit function $\map f {x, y, z}$.
There is clearly one way of doing the above.
Hence the result.
{{qed}}
Theorem: Equation of Cycloid

Consider a circle of radius $a$ rolling without slipping along the x-axis of a cartesian plane.
Consider the point $P$ on the circumference of this circle which is at the origin when its center is on the y-axis.
Consider the cycloid traced out by the point $P$.
Let $\tuple {x, y}$ be the coordinates of $P$ as it travels over the plane.
The point $P = \tuple {x, y}$ is described by the equations:
:$x = a \paren {\theta - \sin \theta}$
:$y = a \paren {1 - \cos \theta}$

Proof:
Let the circle have rolled so that the radius to the point $P = \tuple {x, y}$ is at angle $\theta$ to the vertical.
:700px
The center of the circle is at $\tuple {a \theta, a}$.
From the diagram above, we see:
:The $x$-coordinate is to the left of the center of the circle by $a \sin \theta$
:The $y$-coordinate is below the center of the circle by $a \cos \theta$
It follows that:
:$x = a \theta - a \sin \theta$
:$y = a - a \cos \theta$
whence the result.
{{qed}}
Theorem: Length of Arc of Cycloid

Let $C$ be a cycloid generated by the equations:
:$x = a \paren {\theta - \sin \theta}$
:$y = a \paren {1 - \cos \theta}$
Then the length of one arc of the cycloid is $8 a$.

Proof:
Let $L$ be the length of one arc of the cycloid.
From Arc Length for Parametric Equations:
:$\ds L = \int_0^{2 \pi} \sqrt {\paren {\frac {\d x} {\d \theta} }^2 + \paren {\frac {\d y} {\d \theta} }^2} \rd \theta$
where, from Equation of Cycloid:
:$x = a \paren {\theta - \sin \theta}$
:$y = a \paren {1 - \cos \theta}$
we have:
{{begin-eqn}}
{{eqn | l = \frac {\d x} {\d \theta}
      | r = a \paren {1 - \cos \theta}
      | c = Derivative of Sine Function
}}
{{eqn | l = \frac {\d y} {\d \theta}
      | r = a \sin \theta
      | c = Derivative of Cosine Function
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \paren {\frac {\d x} {\d \theta} }^2 + \paren {\frac {\d y} {\d \theta} }^2
      | r = a^2 \paren {\paren {1 - \cos \theta}^2 + \sin^2 \theta}
      | c = 
}}
{{eqn | r = a^2 \paren {1 - 2 \cos \theta + \cos^2 \theta + \sin^2 \theta}
      | c = 
}}
{{eqn | r = 2 a^2 \paren {1 - \cos \theta}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = 2 a^2 \paren {1 - \cos \theta} \times \frac 2 2
      | c = multiplying top and bottom by $2$ 
}}
{{eqn | r = 4 a^2 \frac {\paren {1 - \cos \theta} } 2
      | c = 
}}
{{eqn | r = 4 a^2 \map {\sin^2} {\theta / 2}
      | c = Half Angle Formula for Sine
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = L
      | r = \int_0^{2 \pi} \sqrt {4 a^2 \map {\sin^2} {\theta / 2} } \rd \theta
      | c = 
}}
{{eqn | r = \int_0^{2 \pi} 2 a \map \sin {\theta / 2} \rd \theta
      | c = 
}}
{{eqn | r = 2 a \int_0^{2 \pi} \map \sin {\theta / 2} \rd \theta
      | c = 
}}
{{eqn | r = 2 a \bigintlimits {-2 \map \cos {\theta / 2} } 0 {2 \pi}
      | c = Primitive of Sine Function
}}
{{eqn | r = 2 a \paren {-2 \map \cos \pi + 2 \map \cos 0 }
      | c = 
}}
{{eqn | r = 2 a \paren {2 + 2 }
      | c = {{cos|0}} {{cos|180}}
}}
{{eqn | r = 8 a
      | c = 
}}
{{end-eqn}}
So $L = 8 a$ where $a$ is the radius of the generating circle.
{{qed}}