avewright/proofwiki-math huggingface dataset:
Theorem: Number of Partitions as Coefficient of Power Series

The number of partitions $\map p n$ of a (strictly) positive integer $n$ is equal to the coefficient of $x^n$ when the expression:
:$\map f n = \dfrac 1 {\paren {1 - x} \paren {1 - x^2} \paren {1 - x^3} \cdots}$
is expanded into a power series.
That is:
:$\map f n = 1 + \map p 1 x + \map p 2 x^2 + \map p 3 x^3 + \cdots$
or:
:$\ds \sum_{n \mathop \in \Z_{\ge 0} } \map p n q^n = \prod_{j \mathop \in \Z_{>0} } \dfrac 1 {1 - q^j}$
where $\map p 0 := 1$.

Proof:
{{begin-eqn}}
{{eqn | l = \map f n
      | r = \dfrac 1 {\paren {1 - x} \paren {1 - x^2} \paren {1 - x^3} \paren {1 - x^4} \cdots}
      | c = 
}}
{{eqn | r = \frac 1 {\paren {1 - x^1} } \times \frac 1 {\paren {1 - x^2} } \times \frac 1 {\paren {1 - x^3} } \times \frac 1 {\paren {1 - x^4} } \times \cdots
      | c = 
}}
{{eqn | r = \paren {1 + x^1 + x^{1 + 1} + x^{1 + 1 + 1} + \cdots} \times \paren {1 + x^2 + x^{2 + 2} + x^{2 + 2 + 2} + \cdots} \times \paren {1 + x^3 + x^{3 + 3} + x^{3 + 3 + 3} + \cdots} \times \paren {1 + x^4 + x^{4 + 4} + x^{4 + 4 + 4} + \cdots} \times \cdots
      | c = Sum of Infinite Geometric Sequence
}}
{{eqn | r = 1 + \paren {x^1 } + \paren {x^{1 + 1} + x^2 } + \paren {x^{1 + 1 + 1} + x^1 x^2 + x^3 } + \paren {x^{1 + 1 + 1 + 1} + x^{1 + 1} x^2 + x^{2 + 2} + x^1 x^3 + x^4} + \cdots
      | c =
}}
{{eqn | r = 1 + \paren {x^1 } + \paren {x^{1 + 1} + x^2 } + \paren {x^{1 + 1 + 1} + x^{1 + 2} + x^3 } + \paren {x^{1 + 1 + 1 + 1} + x^{1 + 1 + 2} + x^{2 + 2} + x^{1 + 3} + x^4} + \cdots
      | c = Product of Powers
}}
{{eqn | r = 1 + \map p 1 x + \map p 2 x^2 + \map p 3 x^3 + \map p 4 x^4 + \cdots
      | c = 
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \map p n x^n
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Suprema Preserving Mapping on Ideals Preserves Directed Suprema

Let $\struct {S, \preceq}$ and $\struct {T, \precsim}$ be ordered sets.
Let $f: S \to T$ be a mapping.
Let every filter $F$ in $\left({S, \preceq}\right)$, $f$ preserve the infimum on $F$.
Then $f$ preserves directed suprema.

Proof:
This follows by {{mutatis}} of the proof of Infima Preserving Mapping on Filters Preserves Filtered Infima.
{{qed}}
Theorem: Mellin Transform of Heaviside Step Function/Lemma

Let $t \in \R$.
Let $s \in \C$ with $\map \Re s < 0$.
Then:
:$\ds \lim_{t \mathop \to +\infty} t^s = 0$

Proof:
Let $s = a + b i$, where $a, b \in \R$, $a<0$.
{{begin-eqn}}
{{eqn | l = \cmod {\lim_{t \mathop \to + \infty} t^s}
      | r = \lim_{t \mathop \to +\infty} \cmod {t^s}
      | c = 
}}
{{eqn | r = \lim_{t \mathop \to +\infty} \cmod {e^{s \ln t} }
      | c = {{Defof|Power to Complex Number}}
}}
{{eqn | r = \lim_{t \mathop \to +\infty} \cmod {e^{\paren {a + b i} \ln t} }
      | c = 
}}
{{eqn | r = \lim_{t \mathop \to +\infty} \cmod {e^{a \ln t} e^{i b \ln t} }
      | c = 
}}
{{eqn | r = \lim_{t \mathop \to +\infty} \cmod {e^{a \ln t} } \cmod {e^{i b \ln t} }
      | c = Modulus of Product
}}
{{eqn | r = \lim_{t \mathop \to +\infty} \cmod {e^{a \ln t} }
      | c = Modulus of Exponential of Imaginary Number is One
}}
{{eqn | r = \lim_{t \mathop \to +\infty} \cmod {t^a}
      | c = {{Defof|Power to Complex Number}}
}}
{{eqn | r = \lim_{t \mathop \to +\infty} \cmod {\dfrac 1 {t^{-a} } }
      | c = 
}}
{{eqn | r = 0
      | c = Sequence of Powers of Reciprocals is Null Sequence
}}
{{eqn | ll= \leadsto
      | l = \lim_{t \mathop \to +\infty} t^s
      | r = 0
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Heaviside Step Function
lkr68xykrt44cfzbwysnx99r41efmzv
Theorem: Up-Complete Lower Bounded Join Semilattice is Complete

Let $\struct {S, \preceq}$ be an up-complete lower bounded join semillattice.
Then $\struct {S, \preceq}$ is complete.

Proof:
Let $X$ be a subset of $S$.
In the case when $X = \O$:
by definition of lower bounded:
:$\exists L \in S: L$ is lower bound for $S$.
By definition of empty set:
:$L$ is upper bound for $X$.
By definition of lower bound:
:$\forall x \in S: x$ is upper bound for $X \implies L \preceq x$
Thus by definition
:$L$ is a supremum of $X$.
Thus:
:$X$ admint a supremum.
{{qed|lemma}}
In the case when $X \ne \O$:
Define
:$Y := \set {\sup A: A \in \map {\operatorname {Fin} } X \land A \ne \O}$
where $\map {\operatorname {Fin} } X$ denotes the set of all finite subsets of $X$.
By Existence of Non-Empty Finite Suprema in Join Semilattice
:all suprema in $Y$ exist,
By definition of non-empty set:
:$Y$ is a non-empty set.
We will prove that
:$Y$ is directed
Let $x, y \in Y$.
By definition of $Y$:
:$\exists A \in \map {\operatorname {Fin} } X \setminus \set \O: x = \sup A$
and
:$\exists B \in \map {\operatorname {Fin} } X \setminus \set \O: y = \sup B$
By Finite Union of Finite Sets is Finite:
:$A \cup B$ is finite
:$A \cup B \ne \O$
By Union is Smallest Superset:
:$A \cup B \subseteq X$
By definition of $Y$:
:$\map \sup {A \cup B} \in Y$
By Set is Subset of Union:
:$A \subseteq A \cup B$ and $B \subseteq A \cup B$
Thus by Supremum of Subset:
:$x \preceq \map \sup {A \cup B}$ and $y \preceq \map \sup {A \cup B}$
Thus by definition:
:$Y$ is directed.
By definition up-complete:
:$Y$ admits a supremum
By definition of supremum
:$\sup Y$ is upper bound for $Y$
We will prove that
:$X \subseteq Y$
Let $x \in X$.
By definitions of subset and singleton:
:$\set x \subseteq X$
:$\set x$ is finite
:$\set x \ne \O$
By definition of $Y$:
:$\sup {\set x} \in Y$
Thus by Supremum of Singleton:
:$x \in Y$
By Upper Bound is Upper Bound for Subset:
:$\sup Y$ is upper bound for $X$
We will prove that
:$\forall x \in S: x$ is upper bound for $X \implies \sup Y \preceq x$
Let $x \in S$ such that
:$x$ is upper bound for $X$
We will prove as sublemma that
:$x$ is upper bound for $Y$
Let $y \in Y$.
By definition of $Y$:
:$\exists A \in \map {\operatorname {Fin} } X \setminus \set \O: y = \sup A$
By definition of $\operatorname {Fin}$:
:$A \subseteq X$
By Upper Bound is Upper Bound for Subset
:$x$ is upper bound for $A$
Thus by definition of supremum:
:$y \preceq x$
Thus by definition
:$x$ is upper bound for $Y$
This ends the proof of sublemma.
Thus by definition of supremum:
:$\sup Y \preceq x$
This ends the proof of lemma.
By definition
:$\sup Y$ is a supremum of $X$
and thus:
:$X$ admits a supremum.
{{qed|lemma}}
Thus result follows by Lattice is Complete iff it Admits All Suprema.
{{qed}}
Theorem: Gregory Series

For $-\dfrac \pi 4 \le \theta \le \dfrac \pi 4$:
:$\theta = \tan \theta - \dfrac 1 3 \tan^3 \theta + \dfrac 1 5 \tan^5 \theta - \ldots$
This is called the '''Gregory series'''.

Proof:
{{begin-eqn}}
{{eqn | l = 1
      | r = \frac {\sec^2 \theta} {\sec^2 \theta}
      | c = 
}}
{{eqn | l = 
      | r = \sec^2 \theta \times \frac 1 {1 - \paren {-\tan^2 \theta} }
      | c = 
}}
{{eqn | l = 
      | r = \sec^2 \theta \times \sum_{n \mathop = 0}^\infty \paren {-\tan^2 \theta}^n
      | c = Sum of Infinite Geometric Sequence
}}
{{eqn | l = 
      | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \sec^2 \theta \tan^{2 n} \theta
      | c =
}}
{{end-eqn}}
By the root test the radius of convergence is $-\dfrac \pi 4 \le \theta \le \dfrac \pi 4$.
{{begin-eqn}}
{{eqn | l = \int \paren {1} \rd \theta
      | r = \int \paren {\sum_{n \mathop = 0} ^ \infty \paren {-1} ^ n \sec ^ 2 \theta \tan ^ {2 n} \theta} \rd \theta
      | c = Integrating both sides
}}
{{eqn | l = \int \rd \theta
      | r = \sum_{n \mathop = 0}^\infty \paren {-1} ^ n \int  \paren { \sec ^ 2 \theta \tan ^ {2 n} \theta} \rd \theta
      | c = 
}}
{{eqn | l = \theta
      | r = \sum_{n \mathop = 0} ^ \infty \frac {\paren {-1} ^ n}{2 n + 1} \tan ^ {2 n + 1} \theta
      | c = Primitive of Power of Tangent of a x by Square of Secant of a x
}}
{{end-eqn}}
{{qed}}
Theorem: Lattice is Complete iff it Admits All Suprema

Let $\struct {S, \preceq}$ be an ordered set.
Then $\struct {S, \preceq}$ is a complete lattice {{iff}}
:$\forall X \subseteq S: X$ admits a supremum.

Proof:
=== Sufficient Condition ===
Let $\struct {S, \preceq}$ be a complete lattice.
Thus by definition of complete lattice:
:$\forall X \subseteq S: X$ admits a supremum.
{{qed|lemma}}
Theorem: Gauss-Bonnet Theorem

Let $M$ be a compact $2$-dimensional Riemannian manifold with boundary $\partial M$.
Let $\kappa$ be the Gaussian curvature of $M$.
Let $k_g$ be the geodesic curvature of $\partial M$.
Then:
:$\ds \int_M \kappa \rd A + \int_{\partial M} k_g \rd s = 2 \pi \map \chi M$
where:
:$\d A$ is the element of area of the surface
:$\d s$ is the line element along $\partial M$
:$\map \chi M$ is the Euler characteristic of $M$.

Proof:
{{ProofWanted}}
{{Namedfor|Carl Friedrich Gauss|name2 = Pierre Ossian Bonnet|cat = Gauss|cat2 = Bonnet}}
Theorem: Unique Factorization Theorem for Gaussian Integers

The ring of Gaussian integers:
:$\struct {\Z \sqbrk i, +, \times}$
forms a unique factorization domain.
That is, every Gaussian integer can be expressed as the product of one or more Gaussian primes, uniquely up to the order in which they appear.

Proof:
We have that:
:Gaussian Integers form Euclidean Domain
:Euclidean Domain is Principal Ideal Domain
:Principal Ideal Domain is Unique Factorization Domain.
So $\struct {\Z \sqbrk i, +, \times}$ forms a unique factorization domain.
Hence the result, by definition of unique factorization domain.
{{qed}}
Theorem: Galois Connection is Expressed by Minimum

Let $\struct {S, \preceq}$, $\struct {T, \precsim}$ be ordered sets.
Let $g: S \to T$, $d: T \to S$ be mappings.
Then $\tuple {g, d}$ is a Galois connection {{iff}}:
:$g$ is an increasing mapping and
::$\forall t \in T: \map d t = \map \min {g^{-1} \sqbrk {t^\succsim} }$
where
:$\min$ denotes the minimum
:$g^{-1} \sqbrk {t^\succsim}$ denotes the image of $t^\succsim$ under relation $g^{-1}$
:$t^\succsim$ denotes the upper closure of $t$

Proof:
=== Sufficient Condition ===
Let $\tuple {g, d}$ be a Galois connection.
Thus by definition of Galois connection:
:$g$ is an increasing mapping
Let $t \in T$.
By definition of reflexivity:
:$\map d t \preceq \map d t$
By definition of Galois connection:
:$t \precsim \map g {\map d t}$
By definition of upper closure:
:$\map g {\map d t} \in t^\succsim$
By definition of image of set under relation:
:$\map d t \in g^{-1} \sqbrk {t^\succsim}$
By definition of lower bound:
:$\forall s \in S: s$ is lower bound for $g^{-1} \sqbrk {t^\succsim} \implies s \preceq \map d t$
We will prove that:
:$\map d t$ is lower bound for $g^{-1} \sqbrk {t^\succsim}$
Let $s \in g^{-1} \sqbrk {t^\succsim}$.
By definition of image of set:
:$\map g s \in t^\succsim$
By definition of upper closure of element:
:$t \precsim \map g s$
Thus by definition of Galois connection:
:$\map d t \preceq s$
By definition of infimum:
:$g^{-1} \sqbrk {t^\succsim}$ admits an infimum
and
:$\map \inf {g^{-1} \sqbrk {t^\succsim} } = \map d t$
Thus:
:$\map d t = \map \min {g^{-1} \sqbrk {t^\succsim} }$
{{qed|lemma}}
Theorem: Closed Form for Pentagonal Numbers

The closed-form expression for the $n$th pentagonal number is:
:$P_n = \dfrac {n \paren {3 n - 1} } 2$

Proof:
Pentagonal numbers are $k$-gonal numbers where $k = 5$.
From Closed Form for Polygonal Numbers we have that:
:$\map P {k, n} = \dfrac n 2 \paren {\paren {k - 2} n - k + 4}$
Hence:
{{begin-eqn}}
{{eqn | l = P_n
      | r = \frac n 2 \paren {\paren {5 - 2} n - 5 + 4}
      | c = Closed Form for Polygonal Numbers
}}
{{eqn | r = \dfrac {n \paren {3 n - 1} } 2
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Closed Form for Hexagonal Numbers

The closed-form expression for the $n$th hexagonal number is:
:$H_n = n \paren {2 n - 1}$

Proof:
Hexagonal numbers are $k$-gonal numbers where $k = 6$.
From Closed Form for Polygonal Numbers we have that:
:$\map P {k, n} = \dfrac n 2 \paren {\paren {k - 2} n - k + 4}$
Hence:
{{begin-eqn}}
{{eqn | l = H_n
      | r = \frac n 2 \paren {\paren {6 - 2} n - 6 + 4}
      | c = Closed Form for Polygonal Numbers
}}
{{eqn | r = n \paren {2 n - 1}
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Sum of Even Integers is Even

The sum of any finite number of even integers is itself even.

Proof:
Proof by induction:
For all $n \in \N$, let $\map P n$ be the proposition:
:The sum of $n$ even integers is an even integer.
$\map P 1$ is trivially true, as this just says:
:The sum of $1$ even integer is an even integer.
The sum of $0$ even integers is understood, from the definition of a vacuous summation, to be $0$, which is even.
So $\map P 0$ is also true.
=== Basis for the Induction ===
$\map P 2$ is the case:
:The sum of any two even integers is itself even.
Consider two even integers $x$ and $y$.
Since they are even, they can be written as $x = 2 a$ and $y = 2 b$ respectively for integers $a$ and $b$.
Therefore, the sum is:
:$x + y = 2 a + 2 b = 2 \paren {a + b}$
Thus $x + y$ has $2$ as a divisor and is even by definition.
This is our basis for the induction.
{{qed|lemma}}
=== Induction Hypothesis ===
Now we need to show that, if $\map P k$ is true, where $k \ge 2$, then it logically follows that $\map P {k + 1}$ is true.
So this is our induction hypothesis:
:The sum of any $k$ even integers is itself even.
Then we need to show:
:The sum of any $k+1$ even integers is itself even.
=== Induction Step ===
This is our induction step:
Consider the sum of any $k + 1$ even integers.
This is the sum of:
:$k$ even integers (which is even by the induction hypothesis)
and:
:another even integer.
That is, it is the sum of two even integers.
By the basis for the induction, this is also even.
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
That is:
:The sum of any finite number of even integers is itself even.
{{qed}}
Theorem: Sum of Even Integers is Even

The sum of any finite number of even integers is itself even.

Proof:
Let $S = \set {r_1, r_2, \ldots, r_n}$ be a set of $n$ even numbers.
By definition of even number, this can be expressed as:
:$S = \set {2 s_1, 2 s_2, \ldots, 2 s_n}$
where:
:$\forall k \in \closedint 1 n: r_k = 2 s_k$
Then:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 1}^n r_k
      | r = \sum_{k \mathop = 1}^n 2 s_k
      | c = 
}}
{{eqn | r = 2 \sum_{k \mathop = 1}^n s_k
      | c = 
}}
{{end-eqn}}
Thus, by definition, $\ds \sum_{k \mathop = 1}^n r_k$ is even.
{{qed}}
Theorem: Galois Connection is Expressed by Maximum

Let $\struct {S, \preceq}$, $\struct {T, \precsim}$ be ordered sets.
Let $g: S \to T$, $d: T \to S$ be mappings.
Then $\tuple {g, d}$ is a Galois connection {{iff}}
:$d$ is an increasing mapping and:
::$\forall s \in S: \map g s = \map \max {d^{-1} \sqbrk {s^\preceq} }$
where:
:$\max$ denotes the maximum
:$d^{-1} \sqbrk {s^\preceq}$ denotes the image of $s^\preceq$ under relation $d^{-1}$
:$s^\preceq$ denotes the lower closure of $s$

Proof:
=== Sufficient Condition ===
Let $\tuple {g, d}$ be a Galois connection.
Thus by definition of Galois connection:
:$d$ is an increasing mapping.
Let $s \in S$.
By definition of reflexivity:
:$\map g s \preceq \map g s$
By definition of Galois connection:
:$\map d {\map g s} \preceq s$
By definition of lower closure:
:$\map d {\map g s} \in s^\preceq$
By definition of image of set under relation:
:$\map g s \in d^{-1} \sqbrk {s^\preceq}$
By definition of upper bound:
:$\forall t \in T: t$ is an upper bound for $d^{-1} \sqbrk {s^\preceq} \implies \map g s \precsim t$
We will prove that:
:$\map g s$ is an upper bound for $d^{-1} \sqbrk {s^\preceq}$
Let $t \in d^{-1} \sqbrk {s^\preceq}$.
By definition of image of set:
:$\map d t \in s^\preceq$
By definition of lower closure of element:
:$\map d t \preceq s$
Thus by definition of Galois connection:
:$t \precsim \map g s$
By definition of supremum:
:$d^{-1} \sqbrk {s^\preceq}$ admits a supremum
and
:$\map \sup {d^{-1} \sqbrk {s^\preceq} } = \map g s$
Thus:
:$\map g s = \map \max {d^{-1} \sqbrk {s^\preceq} }$
{{qed|lemma}}
Theorem: Compass and Straightedge Construction for Regular Heptagon does not exist

There exists no compass and straightedge construction for the regular heptagon.

Proof:
Construction of a regular heptagon is the equivalent of constructing the point $\tuple {\cos \dfrac {2 \pi} 7, \sin \dfrac {2 \pi} 7}$ from the points $\tuple {0, 0}$ and $\tuple {1, 0}$
Let $\epsilon = \map \exp {\dfrac {2 \pi} 7}$.
Then $\epsilon$ is a root of $x^7 - 1$.
We have:
{{begin-eqn}}
{{eqn | l = x^7 - 1
      | r = \paren {x - 1} \paren {x^6 + x^5 + x^4 + x^3 + x^2 + x + 1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \epsilon^6 + \epsilon^5 + \epsilon^4 + \epsilon^3 + \epsilon^2 + \epsilon + 1
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \epsilon^3 + \epsilon^2 + \epsilon + 1 + \epsilon^{-1} + \epsilon^{-2} + \epsilon^{-3}
      | r = 0
      | c = 
}}
{{end-eqn}}
But we have:
{{begin-eqn}}
{{eqn | l = \epsilon
      | r = \cos \dfrac {2 \pi} 7 + i \sin \dfrac {2 \pi} 7
}}
{{eqn | l = \epsilon^{-1}
      | r = \cos \dfrac {2 \pi} 7 - i \sin \dfrac {2 \pi} 7
}}
{{eqn | ll= \leadsto
      | l = \epsilon + \epsilon^{-1}
      | r = 2 c
      | c = where $c = \cos \dfrac {2 \pi} 7$
}}
{{eqn | ll= \leadsto
      | l = \epsilon^2 + \epsilon^{-2} + 2
      | r = 4 c^2
      | c = squaring
}}
{{eqn | ll= \leadsto
      | l = \epsilon^3 + \epsilon^{-3} + 3 \paren {\epsilon + \epsilon^{-1} }
      | r = 8 c^3
      | c = cubing
}}
{{eqn | ll= \leadsto
      | l = \epsilon^2 + \epsilon^{-2}
      | r = 4 c^2 - 2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \epsilon^3 + \epsilon^{-3}
      | r = 8 c^3 - 6 c
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {8 c^3 - 6 c} + \paren {4 c^2 - 2} + 2 c - 1
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 8 c^3 + 4 c^2 - 4 c - 1
      | r = 0
      | c = 
}}
{{end-eqn}}
Thus $2 c$ is a root of the polynomial $x^3 + x^2 - 2 x - 1$
But from Irreducible Polynomial: $x^3 + x^2 - 2 x - 1$ in Rationals:
:$x^3 + x^2 - 2 x - 1$ is irreducible over $\Q$.
Thus by Algebraic Element of Degree 3 is not Element of Field Extension of Degree Power of 2, $\cos \dfrac {2 \pi} 7$ 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: Integer to Rational Power is Irrational iff not Integer or Reciprocal

Let $m$ be a rational number.
Let $n$ be a positive integer.
Then $n^m$ is an irrational number {{iff}} $n^{\size m}$ is not an integer.

Proof:
=== Necessary Condition ===
Let $n^{\size m} \notin \Z$.
We have that:
:$n^m = n^{u/v}$ for some $u \in\Z$ and $v \in \Z_{\ne 0}$
Then it follows from the definition of a rational power and the existence of a real $v$th root of $n^u$ that:
:$n^m = n^{u/v} = \paren {n^u}^{1/v} \in \R$
{{AimForCont}} $n^m \in \Q$.
We have that:
:$\size m = 0 \implies n^{\size m} \in \Z$
It follows that:
:$\size m > 0$
Then:
:$\size m > 0$
:$m \in \Q$
:$n^{\size m} > 0$
:$n^m \in \Q$
imply that
:$n^{\size m} = n^{p/q} = \dfrac r s$
for some $\tuple {p, q, r, s} \in \Z_{>0}^4$ where $r$ and $s$ have no common prime factors.
Raising both sides of $n^{p/q} = \dfrac r s$ to the power of $q$ yields:
:$n^p = \dfrac {r^q} {s^q}$
We have that:
:$\dfrac {r^q} {s^q} = n^p \in \Z$
Hence $r^q$ is divisible by $s^q$.
By the Fundamental Theorem of Arithmetic, $r^q$ and $s^q$ have the same prime factors as $r$ and $s$ respectively.
But we have that:
:$s^q \divides r^q$
and:
:$s \ne 1$
imply that $r$ and $s$ have a common prime factor.
But this would contradict the fact that $r$ and $s$ have no common prime factors.
Therefore $s = 1$.
Then:
:$n^{\size m} = \dfrac r s$
and:
:$s = 1$
imply that:
:$r = n^{\size m} \notin \Z$
From this contradiction it follows that:
:$n^m \notin \Q$
and since $n^m \in \R$:
:$n^m \in \R \setminus \Q$
That is, $n^m$ is an irrational number.
{{qed|lemma}}
Theorem: Area Enclosed by First Turn of Archimedean Spiral

Let $S$ be the Archimedean spiral defined by the equation:
:$r = a \theta$
The area $\AA$ enclosed by the first turn of $S$ and the polar axis is given by:
:$\AA = \dfrac {4 \pi^3 a^2} 3$
:500px

Proof:
{{begin-eqn}}
{{eqn | l = \AA
      | r = \int_0^{2 \pi} \frac {\paren {a \theta}^2} 2 \rd \theta
      | c = Area between Radii and Curve in Polar Coordinates
}}
{{eqn | r = \intlimits {\frac {a^2 \theta^3} 6} 0 {2 \pi}
      | c = Primitive of Power
}}
{{eqn | r = \frac {\paren {2 \pi}^3 a^2} 6
      | c = 
}}
{{eqn | r = \frac {4 \pi^3 a^2} 3
      | c = after simplification
}}
{{end-eqn}}
{{qed}}
Theorem: Trisecting the Angle/Archimedean Spiral

Let $\alpha$ be an angle which is to be trisected.
This can be achieved by means of an Archimedean spiral.

Proof:
Let the equation of the Archimedean spiral be $r = a \theta$.
Then:
{{begin-eqn}}
{{eqn | l = \angle DOB
      | r = \frac {OD} a
}}
{{eqn | r = \frac {OA/3} a
}}
{{eqn | r = \frac 1 3 \angle AOB
}}
{{end-eqn}}
{{qed}}
Theorem: Archimedes' Limits to Value of Pi

The value of $\pi$ lies between $3 \frac {10} {71}$ and $3 \frac 1 7$:
:$3 \dfrac {10} {71} < \pi < 3 \dfrac 1 7$

Proof:
Let $O$ be a circle with diameter $AB = 1$
Let $Q$ be the circumference of $O$.
By the definition of $\pi$:
:$\dfrac Q {AB} = \pi$
Since $AB = 1$ then $Q$ is exactly $\pi$.
Using regular polygons inscribed and circumscribed about the circle $O$, we aim to demonstrate that the bounds on $\pi$ are:
:$\dfrac {223} {71} < \pi < \dfrac {22} {7}$
=== Lemma 1 ===
{{:Archimedes' Limits to Value of Pi/Lemma 1}}
=== Lemma 2 ===
{{:Archimedes' Limits to Value of Pi/Lemma 2}}
=== Lemma 3 ===
{{:Archimedes' Limits to Value of Pi/Lemma 3}}
=== Lemma 4 ===
{{:Archimedes' Limits to Value of Pi/Lemma 4}}
Combining the two results from the fifth iteration of {{Lemma|Archimedes' Limits to Value of Pi|3}} and {{Lemma|Archimedes' Limits to Value of Pi|4}}, we have:
{{begin-eqn}}
{{eqn | l = 3 \tfrac {10} {71}
      | o = <
      | m = \pi
      | mo= <
      | r = 3 \tfrac 1 7
}}
{{eqn | ll= \leadsto
      | l = \dfrac {223} {71}
      | o = <
      | m = \pi
      | mo= <
      | r = \dfrac {22} 7
}}
{{end-eqn}}
Expressing this in decimal:
:$3.1408 < \pi < 3.1429$
{{qed}}
Theorem: Upper Adjoint Preserves All Infima

Let $\left({S, \preceq}\right)$, $\left({T, \precsim}\right)$ be ordered sets.
Let $g: S \to T$ be an upper adjoint of Galois connection.
Then $g$ preserves all infima.

Proof:
By definition of upper adjoint
:$\exists d: T \to S: \left({g, d}\right)$ is a Galois connection
Let $X$ be a subset of $S$ such that
:$X$ admits an infimum.
We will prove as lemma 1 that
:$\forall t \in T: t$ is lower bound for $g^\to\left({X}\right) \implies t \precsim g\left({\inf X}\right)$
Let $t \in T$ such that
:$t$ is lower bound for $g^\to\left({X}\right)$
We will prove as sublemma that
:$d\left({t}\right)$ is lower bound for $X$
Let $s \in X$.
By definition of image of set:
:$g\left({s})\right) \in g^\to\left({X}\right)$
By definition of lower bound:
:$t \precsim g\left({s}\right)$
Thus by definition of Galois connection:
:$d\left({t}\right) \preceq s$
This ends the proof of sublemma.
By definition of infimum:
:$d\left({t}\right) \preceq \inf X$
Thus by definition of Galois connection:
:$t \precsim g\left({\inf X}\right)$
This ends the proof of lemma 1.
We will prove as lemma 2 that
:$g\left({\inf X}\right)$ is lower bound for $g^\to\left({X}\right)$
Let $t \in g^\to\left({X}\right)$.
By definition of image of set:
:$\exists s \in S: s \in X \land g\left({s}\right) = t$
By definition of infimum:
:$\inf X$ is lower bound for $X$
By definition of lower bound:
:$\inf X \preceq s$
By definition of Galois connection:
:$g$ is increasing mapping.
Thus by definition of increasing mapping:
:$g\left({\inf X}\right) \precsim t$
This ends the proof of lemma 2.
Thus by definition of infimum:
:$g^\to\left({X}\right)$ admits an infimum
and
:$\inf\left({g^\to\left({X}\right)}\right) = g\left({\inf X}\right)$
Thus by definition:
:$g$ preserves infimum on $X$
Thus by definition:
:$g$ preserves all infima.
{{qed}}