avewright/proofwiki-math huggingface dataset:
Theorem: Relative Pseudocomplement and Shift Mapping form Galois Connection in Brouwerian Lattice

Let $\struct {S, \vee, \wedge, \preceq}$ be a Brouwerian lattice.
Let $a$ be an element of $S$.
Let $g, d: S \to S$ be mappings such that:
:$\forall s \in S: \map g s = a \to s$
and
:$\forall s \in S: \map d s = a \wedge s$
Then $\struct {g, d}$ is a Galois connection.

Proof:
By Brouwerian Lattice iff Shift Mapping is Lower Adjoint:
:$d$ is lower adjoint
By definition of lower adjoint:
:$\exists g': S \to S: \struct {g', d}$ is Galois connection
By Galois Connection is Expressed by Maximum:
:$\forall s \in S: \map {g'} s = \map \max {d^{-1} \sqbrk {s^\preceq} }$
By definition of image of set:
:$\forall s \in S: \map {g'} s = \map \max {\set {x \in S: \map d x \in s^\preceq} }$
By definition of lower closure of element:
:$\forall s \in S: \map {g'} s = \map \max {\set {x \in S: \map d x \preceq s} }$
By definition of $d$:
:$\forall s \in S: \map {g'} s = \map \max {\set {x \in S: a \wedge x \preceq s} }$
By definition of relative pseudocomplement:
:$\forall s \in S: \map {g'} s = a \to s = \map g s$
By Equality of Mappings:
:$g = g'$
Hence
:$\struct {g, d}$ is a Galois connection.
{{qed}}
Theorem: Inequality with Meet Operation is Equivalent to Inequality with Relative Pseudocomplement in Brouwerian Lattice

Let $\struct {S, \vee, \wedge, \preceq}$ be s Brouwerian lattice.
Let $a, x, y \in S$.
Then
:$a \wedge x \preceq y$ {{iff}} $x \preceq a \to y$

Proof:
Define a mapping $d: S \to S$:
:$\forall s \in S: \map d s = a \wedge s$
Define a mapping $g: S \to S$:
:$\forall s \in S: \map g s = a \to s$
By Relative Pseudocomplement and Shift Mapping form Galois Connection in Brouwerian Lattice:
:$\tuple {g, d}$ is Galois connection.
By definition of Galois connection:
:$x \preceq \map g y$ {{iff}} $\map d x \preceq y$
Thus by definitions of $g$ and $d$:
:$a \wedge x \preceq y$ {{iff}} $x \preceq a \to y$
{{qed}}
Theorem: Weierstrass Approximation Theorem

Let $f$ be a real function which is continuous on the closed interval $\Bbb I = \closedint a b$.
Then $f$ can be uniformly approximated on $\Bbb I$ by a polynomial function to any given degree of accuracy.

Proof:
Let $\AA \subseteq \map C {\Bbb I, \R}$ be the set of real polynomial functions.
$\AA$ is a subalgebra of $\map C {\Bbb I, \R}$ because polynomials over $\R$ form an algebra over $\R$.
Let $I$ denote the identity mapping on $\Bbb I$, i.e.:
:$\forall x \in \Bbb I : \map I x = x$
Then $I \in \AA$.
Thus $\AA$ separates the points of $\Bbb I$, since trivially:
:$\forall x,y \in \Bbb I : x \ne y \implies \map I x \ne \map I y$
It is also clear that $1 \in \AA$.
Therefore the claim follows from Stone-Weierstrass Theorem.
{{qed}}
Theorem: Construction of Right Angle by Stretched Rope

Let a rope be knotted at regular intervals so that there are $12$ equal segments separated by knots.
Tie the rope in a loop consisting of those $12$ segments.
Fix one of the knots to the ground at the point you want the right angle to be placed.
Stretch the rope tightly in the direction of one of the legs of the right angle you want to create and fix the fourth knot to the ground.
Stretch the rope tightly in the direction of the other leg of the right angle you want to create and fix the third knot in the ground, at the same time making sure the remaining segment of $5$ knots is also tight.
The point where the $3$-knot section and the $4$-knot section meet, the rope will be bent at a right angle.
:400px

Proof:
The rope will be stretched in the form of a triangle with sides $3$, $4$ and $5$.
We have that:
:$3^2 + 4^2 = 9 + 16 = 25 = 5^2$
and so by Pythagoras's Theorem the triangle is right angled.
{{qed}}
Theorem: Top equals to Relative Pseudocomplement in Brouwerian Lattice

Let $\struct {S, \vee, \wedge, \preceq}$ be a Brouwerian lattice with greatest element $\top$.
Let $a, b \in S$.
Then
:$\top = a \to b$ {{iff}} $a \preceq b$

Proof:
=== Sufficient Condition ===
Let:
:$\top = a \to b$
By definition of reflexivity:
:$\top \preceq a \to b$
By Inequality with Meet Operation is Equivalent to Inequality with Relative Pseudocomplement in Brouwerian Lattice:
:$\top \wedge a \preceq b$
Thus
:$a \preceq b$
{{qed|lemma}}
Theorem: Up-Complete Product

Let $\struct {S, \preceq_1}$, $\struct {T, \preceq_2}$ be non-empty ordered sets.
Let $\struct {S \times T, \preceq}$ be the simple order product of $\struct {S, \preceq_1}$ and $\struct {T, \preceq_2}$.

Proof:
=== Lemma 1 ===
{{:Up-Complete Product/Lemma 1}}{{qed|lemma}}
Theorem: Motion of Rocket in Outer Space

Let $B$ be a rocket travelling in outer space.
Let the velocity of $B$ at time $t$ be $\mathbf v$.
Let the mass of $B$ at time $t$ be $m$.
Let the exhaust velocity of $B$ be constant at $\mathbf b$.
Then the equation of motion of $B$ is given by:
:$m \dfrac {\d \mathbf v} {\d t} = - \mathbf b \dfrac {\d m} {\d t}$

Proof:
From Motion of Body with Variable Mass:
:$(1): \quad \mathbf w \dfrac {\d m} {\d t} + \mathbf F = m \dfrac {\d \mathbf v} {\d t}$
where:
:$\mathbf F$ is the external force being applied
:$\mathbf w$ is the velocity of the added mass relative to $B$.
In this scenario:
:there is no external force and so $\mathbf F = \mathbf 0$
:the velocity of the added mass relative to $B$ is $-\mathbf b$.
Thus $(1)$ becomes:
:$-\mathbf b \dfrac {\d m} {\d t} = m \dfrac {\d \mathbf v} {\d t}$
{{qed}}
Theorem: Motion of Rocket in Outer Space

Let $B$ be a rocket travelling in outer space.
Let the velocity of $B$ at time $t$ be $\mathbf v$.
Let the mass of $B$ at time $t$ be $m$.
Let the exhaust velocity of $B$ be constant at $\mathbf b$.
Then the equation of motion of $B$ is given by:
:$m \dfrac {\d \mathbf v} {\d t} = - \mathbf b \dfrac {\d m} {\d t}$

Proof:
From Newton's Second Law of Motion:
:$\mathbf F = \dfrac \d {\d t} \paren {m \mathbf v}$
At time $t + \Delta t$, let:
: the mass of $B$ be $m + \Delta m$
: the velocity of $B$ be $\mathbf v + \Delta \mathbf v$.
The fuel is being consumed, so the increase in mass of the fuel during time $\Delta t$ is $-\Delta m$.
Thus the exhaust products, therefore of mass $-\Delta m$, are expelled at a velocity $-\mathbf b$ relative to $B$.
Thus this material is actually moving at a velocity $\mathbf v - \mathbf b$.
By Principle of Conservation of Linear Momentum, the total linear momentum is constant.
Thus:
{{begin-eqn}}
{{eqn | l = m \mathbf v
      | r = \paren {m + \Delta m} \paren {\mathbf v + \Delta \mathbf v} + \paren {-\Delta m} \paren {\mathbf v - \mathbf b}
      | c = 
}}
{{eqn | r = m \mathbf v + m \Delta \mathbf v + \paren {\Delta m} \mathbf v + \Delta m \Delta \mathbf v - \paren {-\Delta m} \mathbf v + \Delta m \mathbf b
      | c = 
}}
{{eqn | ll= \leadsto
      | l = m \Delta \mathbf v
      | r = - \Delta m \paren {\mathbf b + \Delta \mathbf v}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = m \frac {\Delta \mathbf v} {\Delta t}
      | r = - \frac {\Delta m} {\Delta t} \paren {\mathbf b + \Delta \mathbf v}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = m \frac {\d \mathbf v} {\d t}
      | r = - \mathbf b \frac {\d m} {\d t}
      | c = letting $\Delta t \to 0$
}}
{{end-eqn}}
{{qed}}
Theorem: Velocity of Rocket in Outer Space

Let $B$ be a rocket travelling in outer space.
Let the velocity of $B$ at time $t$ be $\mathbf v$.
Let the mass of $B$ at time $t$ be $m$.
Let the exhaust velocity of $B$ be constant at $\mathbf b$.
Then the velocity of $B$ at time $t$ is given by:
:$\map {\mathbf v} t = \map {\mathbf v} 0 + \mathbf b \ln \dfrac {\map m 0} {\map m t}$
where $\map {\mathbf v} 0$ and $\map m 0$ are the velocity and mass of $B$ at time $t = 0$.

Proof:
From Motion of Rocket in Outer Space, the equation of motion of $B$ is given by:
:$m \dfrac {\d \mathbf v} {\d t} = -\mathbf b \dfrac {\d m} {\d t}$
Hence:
{{begin-eqn}}
{{eqn | l = \int_0^t \dfrac {\d \mathbf v} {\d t} \rd t
      | r = -\int_0^t \mathbf b \frac 1 m \dfrac {\d m} {\d t} \rd t
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \int_{t \mathop = 0}^t \rd \mathbf v
      | r = -\int_{t \mathop = 0}^t \mathbf b \dfrac {\d m} m
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \bigintlimits {\mathbf v} 0 t
      | r = -\mathbf b \bigintlimits {\ln m} 0 t
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {\mathbf v} t - \map {\mathbf v} 0
      | r = -\mathbf b \paren {\map {\ln m} t - \map {\ln m} 0}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {\mathbf v} t
      | r = \map {\mathbf v} 0 + \mathbf b \ln \dfrac {\map m 0} {\map m t}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Acceleration of Rocket in Outer Space

Let $B$ be a rocket travelling in outer space.
Let the velocity of $B$ at time $t$ be $\mathbf v$.
Let the mass of $B$ at time $t$ be $m$.
Let the exhaust velocity of $B$ be constant at $\mathbf b$.
Then the acceleration of $B$ at time $t$ is given by:
:$\mathbf a = \dfrac 1 m \paren {-\mathbf b \dfrac {\d m} {\d t} }$

Proof:
From Motion of Rocket in Outer Space, the equation of motion of $B$ is given by:
:$(1): \quad m \dfrac {\d \mathbf v} {\d t} = -\mathbf b \dfrac {\d m} {\d t}$
By definition, the acceleration of $B$ is its rate of change of velocity:
:$\mathbf a = \dfrac {\d \mathbf v} {\d t}$
The result follows by substituting $\mathbf a$ for $\dfrac {\d \mathbf v} {\d t}$ and dividing by $m$.
{{qed}}
Theorem: Up-Complete Product/Lemma 1

Let $X$ be a directed subset of $S$.
Let $Y$ be a directed subset of $T$.
Then $X \times Y$ is also a directed subset of $S \times T$.

Proof:
Let $\tuple {s_1, t_1}, \tuple {s_2, t_2} \in X \times Y$.
By definition of Cartesian product:
:$s_1, s_2 \in X$ and $t_1, t_2 \in Y$
By definition of directed subset:
:$\exists h_1 \in X: s_1 \preceq_1 h_1 \land s_2 \preceq_1 h_1$
and
:$\exists h_2 \in X: t_1 \preceq_2 h_2 \land t_2 \preceq_2 h_2$
By definition of simple order product:
:$\exists \tuple {h_1, h_2} \in X \times Y: \tuple {s_1, t_1} \preceq \tuple {h_1, h_2} \land \tuple {s_2, t_2} \preceq \tuple {h_1, h_2}$
Thus by definition:
:$X \times Y$ is a directed subset of $S \times T$.
{{qed}}
Theorem: Up-Complete Product/Lemma 2

Let $X$ be a directed subset of $S \times T$.
Then
:$\map {\pr_1^\to} X$ and $\map {\pr_2^\to} X$ are directed
where 
:$\pr_1$ denotes the first projection on $S \times T$
:$\pr_2$ denotes the second projection on $S \times T$
:$\map {\pr_1^\to} X$ denotes the image of $X$ under $\pr_1$

Proof:
Let $x, y \in \map {\pr_1^\to} X$.
By definitions of image of set and projections:
:$\exists x' \in T: \tuple {x, x'} \in X$
and
:$\exists y' \in T: \tuple {y, y'} \in X$
By definition of directed:
:$\exists \tuple {a, b} \in X: \tuple {x, x'} \preceq \tuple {a, b} \land \tuple {y, y'} \preceq \tuple {a, b}$
By definition of simple order product:
:$\exists a \in \map {\pr_1^\to} X: x \preceq_1 a \land y \preceq_1 a$
Thus by definition:
:$\map {\pr_1^\to} X$ is directed.
By {{mutatis}}:
:$\map {\pr_2^\to} X$ is directed.
{{qed}}
Theorem: Lagrange's Trigonometric Identities/Cosine

{{begin-eqn}}
{{eqn | l = \frac 1 2 + \sum_{k \mathop = 1}^n \map \cos {k x}
      | r = \frac 1 2 + \cos x + \cos 2 x + \cos 3 x + \cdots + \cos n x
      | c = 
}}
{{eqn| r = \frac {\map \sin {\paren {2 n + 1} x / 2} } {2 \map \sin {x / 2} }
      | c = 
}}
{{end-eqn}}
where $x$ is not an integer multiple of $2 \pi$.

Proof:
By the Werner Formula for Cosine by Sine:
:$2 \cos \alpha \sin \beta = \map \sin {\alpha + \beta} - \map \sin {\alpha - \beta}$
Thus we establish the following sequence of identities:
{{begin-eqn}}
{{eqn | l = 2 \cdot \frac 1 2 \sin \frac x 2
      | r = \sin \frac x 2
      | c = 
}}
{{eqn | l = 2 \cos x \sin \frac x 2
      | r = \sin \frac {3 x} 2 - \sin \frac x 2
      | c = 
}}
{{eqn | l = 2 \cos 2 x \sin \frac x 2
      | r = \sin \frac {5 x} 2 - \sin \frac {3 x} 2
      | c = 
}}
{{eqn | o = \cdots
      | c = 
}}
{{eqn | l = 2 \cos n x \sin \frac x 2
      | r = \sin \frac {\paren {2 n + 1} x} 2 - \sin \frac {\paren {2 n - 1} x} 2
      | c = 
}}
{{end-eqn}}
Summing the above:
:$\ds 2 \sin \frac x 2 \paren {\frac 1 2 + \sum_{k \mathop = 1}^n \map \cos {k x} } = \sin \frac {\paren {2 n + 1} x} 2$
as the sums on the {{RHS}} form a telescoping series.
The result follows by dividing both sides by $2 \sin \dfrac x 2$.
It is noted that when $x$ is a multiple of $2 \pi$ then:
:$\sin \dfrac x 2 = 0$
leaving the {{RHS}} undefined.
{{qed}}
Theorem: Eratosthenes' Measurement of Earth

The circumference of Earth was measured by {{AuthorRef|Eratosthenes of Cyrene}} to be of the order of $45 \, 000 \, \mathrm{km}$.

Proof:
:700px
We have that the shape of the Earth is very close to being a sphere.
In the diagram, we have a great circle of Earth with center $O$ and radius $R$.
We have the cities of Alexandria, Egypt ($A$) and Syene, Egypt ($S$) lie on approximately the same meridian.
We have the distance $D$ between $A$ and $S$ is $5\,000$ stadia.
We have the difference in latitude between $A$ and $S$ as angle $\angle AOS$.
We have that on the summer solstice at $S$, sundial gnomons cast no shadows and the bottoms of deep wells are lit.
Therefore, the Sun is at zenith over Syene on the summer solstice.
We have that, on the same day at $A$, a sundial gnomon $\overline {A G}$ casts a shadow $\overline {A H}$ indicating that the angle of the Sun from zenith $\angle AGH$ is about $7 \degrees$.
We have that the distance to the Sun is very much larger than the radius of Earth and the radius of Sun.
Therefore, the rays of light $L_A$ and $L_S$ that fall on $A$ and $S$, respectively, are parallel.
By Parallelism implies Equal Alternate Angles, we have
:$\angle AOS = \angle AGH$
Since the angle $\angle AOS$ is $7 / 360 \approx 1 / 50$ of the Measurement of Full Angle, the distance from $A$ to $S$ must be $\approx 1 / 50$ of the Earth's circumference.
Therefore, the circumference of the Earth is:
{{begin-eqn}}
{{eqn | l = \frac C D
      | r = \frac {360 \degrees} {7 \degrees}
}}
{{eqn | o = \approx
      | r = \frac {50} 1
}}
{{eqn | ll = \leadsto
      | l = C
      | r = 50 D
}}
{{eqn | r = 50 \times 5 \, 000 \, \textrm {stadia}
}}
{{eqn | o = \approx
      | r = 250 \, 000 \, \textrm {stadia}
}}
{{end-eqn}}
{{qed}}
{{Namedfor|Eratosthenes of Cyrene|cat = Eratosthenes}}
Theorem: Existence of Prime-Free Sequence of Natural Numbers

Let $n$ be a natural number.
Then there exists a sequence of consecutive natural numbers of length $n$ which are all composite.

Proof:
Consider the number:
:$N := \paren {n + 1}!$
where $!$ denotes the factorial.
Let $i \in I$ where:
:$I = \set {i \in \N: 2 \le i \le n + 1}$
We have that $\size I = n$.
Then for all $i \in I$:
{{begin-eqn}}
{{eqn | l = i
      | o = \divides
      | r = N
      | c = where $\divides$ denotes divisibility
}}
{{eqn | ll= \leadsto
      | l = i
      | o = \divides
      | r = N + i
      | c = 
}}
{{end-eqn}}
and so $N + i$ is composite.
That is:
:$N + 2, N + 3, \ldots, N + n, N + n + 1$
are all composite.
{{qed}}
Theorem: Approximate Value of Nth Prime Number

The $n$th prime number is approximately $n \ln n$.

Proof:
This will be demonstrated by showing that:
:$\ds \lim_{n \mathop \to \infty} \dfrac {p_n} {n \ln n} = 1$
where $p_n$ denotes the $n$th prime number.
By definition of prime-counting function:
:$\map \pi {p_n} = n$
The Prime Number Theorem gives:
:$\ds \lim_{x \mathop \to \infty} \dfrac {\map \pi x} {x / \ln x} = 1$
Thus:
:$\ds \lim_{x \mathop \to \infty} \dfrac n {p_n / \ln p_n} = 1$
{{begin-eqn}}
{{eqn | l = \lim_{x \mathop \to \infty} \dfrac {\map \pi x} {x / \ln x}
      | r = 1
      | c = Prime Number Theorem
}}
{{eqn | ll= \leadsto
      | l = \lim_{n \mathop \to \infty} \dfrac n {p_n / \ln p_n}
      | r = 1
      | c = {{Defof|Prime-Counting Function}}
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = \lim_{n \mathop \to \infty} \dfrac {p_n} {n \ln p_n}
      | r = 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \lim_{n \mathop \to \infty} \paren {\ln p_n - \ln n - \ln \ln p_n}
      | r = 0
      | c = Logarithm of both sides
}}
{{eqn | ll= \leadsto
      | l = \lim_{n \mathop \to \infty} \ln p_n \paren {1 - \frac {\ln n} {\ln p_n} - \frac {\ln \ln p_n} {\ln p_n} }
      | r = 0
      | c = multiplying argument through by $\ln p_n$
}}
{{eqn | ll= \leadsto
      | l = \lim_{n \mathop \to \infty} \ln p_n \paren {1 - \frac {\ln n} {\ln p_n} }
      | r = 0
      | c = as $\dfrac {\ln n} n \to 0$
}}
{{eqn | ll= \leadsto
      | l = \lim_{n \mathop \to \infty} \paren {1 - \frac {\ln n} {\ln p_n} }
      | r = 0
      | c = as $\ln p_n \ne 0$
}}
{{eqn | ll= \leadsto
      | l = \lim_{n \mathop \to \infty} \frac {\ln n} {\ln p_n}
      | r = 1
      | c = as $\ln p_n \ne 0$
}}
{{eqn | ll= \leadsto
      | l = \lim_{n \mathop \to \infty} \dfrac {p_n} {n \ln n} 
      | r = \lim_{n \mathop \to \infty} \dfrac {p_n} {n \ln p_n} \frac {\ln p_n} {\ln n}
      | c = from $(1)$
}}
{{eqn | r = 1
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Prime Number Theorem in Eulerian Logarithmic Integral Form

The Prime Number Theorem is equivalent to:
:$\ds \lim_{x \mathop \to \infty} \frac {\map \pi x} {\map \Li x} = 1$
where:
:$\map \pi x$ is the prime-counting function
:$\map \Li x$ is the Eulerian logarithmic integral:
::$\ds \map \Li x := \int_2^x \dfrac {\d t} {\ln t}$

Proof:
Using Integration by Parts:
{{begin-eqn}}
{{eqn | l = \map \Li x
      | r = \int_2^x \dfrac {\d t} {\ln t}
      | c = 
}}
{{eqn | n = 1
      | r = \dfrac x {\ln x} - \dfrac 2 {\ln 2} + \int_2^x \dfrac {\d t} {\paren {\ln t}^2}
      | c = 
}}
{{end-eqn}}
We have that $\dfrac 1 {\paren {\ln t}^2}$ is positive and decreasing for $t > 1$.
Let $x \ge 4$.
Then:
{{begin-eqn}}
{{eqn | l = 0
      | o = <
      | r = \int_2^x \dfrac {\d t} {\paren {\ln t}^2}
      | c = 
}}
{{eqn | r = \int_2^{\sqrt x} \dfrac {\d t} {\paren {\ln t}^2} + \int_{\sqrt x}^x \dfrac {\d t} {\paren {\ln t}^2}
      | c = 
}}
{{eqn | o = <
      | r = \dfrac {\sqrt x - 2} {\paren {\ln 2}^2} + \dfrac {x - \sqrt x} {\paren {\ln \sqrt x}^2}
      | c = 
}}
{{eqn | o = <
      | r = \dfrac {\sqrt x} {\paren {\ln 2}^2} + \dfrac {4 x} {\paren {\ln \sqrt x}^2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 0
      | o = <
      | r = \dfrac {\ds \int_2^x \frac {\d t} {\paren {\ln t}^2} } {x / \ln x}
      | c = 
}}
{{eqn | o = <
      | r = \dfrac {\ln x} {\sqrt x \paren {\ln 2}^2} + \frac 4 {\ln x}
      | c = 
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = \lim_{x \mathop \to \infty} \dfrac {\ds \int_2^x \frac {\d t} {\paren {\ln t}^2} } {x / \ln x}
      | r = 0
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \frac {\map \Li x} {x / \ln x}
      | r = \dfrac {\dfrac x {\ln x} - \dfrac 2 {\ln 2} + \ds \int_2^x \dfrac {\d t} {\paren {\ln t}^2} } {x / \ln x}
      | c = from $(1)$
}}
{{eqn | r = 1 - \dfrac {2 \ln x} {x \ln 2} + \dfrac {\ds \int_2^x \frac {\d t} {\paren {\ln t}^2} } {x / \ln x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \lim_{x \mathop \to \infty} \frac {\map \Li x} {x / \ln x}
      | r = 1 - \lim_{x \mathop \to \infty} \dfrac 2 {\ln 2} \dfrac x {\ln x} - 0
      | c = from $(2)$
}}
{{eqn | n = 3
      | ll= \leadsto
      | l = \lim_{x \mathop \to \infty} \frac {\map \Li x} {x / \ln x}
      | r = 1
      | c = as $\ds \lim_{x \mathop \to \infty} \dfrac x {\ln x} = 0$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \lim_{x \mathop \to \infty} \frac {\map \pi x} {x / \ln x}
      | r = \lim_{x \mathop \to \infty} \frac {\map \pi x} {\map \Li x} \frac {\map \Li x} {x / \ln x}
      | c = 
}}
{{eqn | r = \lim_{x \mathop \to \infty} \frac {\map \pi x} {\map \Li x}
      | c = from $(3)$
}}
{{end-eqn}}
{{qed}}
Theorem: Exponential of Rational Number is Irrational

Let $r$ be a rational number such that $r \ne 0$.
Then:
:$e^r$ is irrational
where $e$ is Euler's number.

Proof:
Let $r = \dfrac p q$ be rational such that $r \ne 0$.
{{AimForCont}} $e^r$ is rational.
Then $\paren {e^r}^q = e^p$ is also rational.
Then if $e^{-p}$ is rational, it follows that $e^p$ is rational.
It is therefore sufficient to derive a contradiction from the supposition that $e^p$ is rational for every $p \in \Z_{>0}$.
Let $e^p = \dfrac a b$ for $a, b \in \Z_{>0}$.
Let $n \in \Z_{>0}$ be a strictly positive integer.
Let $\map f x$ be the function defined as:
{{begin-eqn}}
{{eqn | n = 1
      | l = \map f x
      | o = :=
      | r = \frac {x^n \paren {1 - x}^n} {n!}
      | c = 
}}
{{eqn | r = \frac 1 {n!} \sum_{k \mathop = n}^{2 n} c_k x^k
      | c = where the $c_k$'s are some integers
}}
{{end-eqn}}
Note that:
:$(2): \quad 0 < x < 1 \implies 0 < \map f x < \dfrac 1 {n!}$
We also have:
:$\map f 0 = 0$
:$\map {f^{\paren m} } 0 = 0$ if $m < n$ or $m > 2 n$
and:
:$n \le m \le 2 n \implies \map {f^{\paren m} } 0 = \dfrac {m!} {n!} c_m$
and this number is an integer.
Thus at $x = 0$, $\map f x$ and all its derivatives are integers.
Since $\map f {1 - x} = \map f x$, the same is true for $x = 1$.
Let $\map F x$ be the function defined as:
{{begin-eqn}}
{{eqn | n = 3
      | l = \map F x
      | o = :=
      | r = \sum_{k \mathop = 0}^{2 n} \paren {-1}^k p^{2 n - k} \map {f^{\paren k} } x
      | c = 
}}
{{eqn | r = p^{2 n} \map f x - p^{2 n - 1} \map {f'} x + p^{2 n - 2} \map {f''} x - \cdots - p \map {f^{\paren {2 n - 1} } } x + \map {f^{\paren {2 n} } } x
      | c = 
}}
{{end-eqn}}
Because of the properties of $\map f x$ and its derivatives above, $\map F 0$ and $\map F 1$ are integers.
Next we have:
{{begin-eqn}}
{{eqn | n = 4
      | l = \map {\frac {\d} {\d x} } {e^{p x} \map F x}
      | r = e^{p x} \paren {\map {F'} x + p \, \map F x}
      | c = 
}}
{{eqn | r = p^{2 n + 1} e^{p x} \map f x
      | c = from $\map {F'} x + p \, \map F x$ based on $(3)$
}}
{{end-eqn}}
$(4)$ leads to:
{{begin-eqn}}
{{eqn | l = b \int_0^1 p^{2 n + 1} e^{p x} \map f x \d x
      | r = b \bigintlimits {e^{p x} \map F x} 0 1
      | c = 
}}
{{eqn | r = a \, \map F 1 - b \, \map F 0
      | c = 
}}
{{end-eqn}}
which is an integer.
But from $(2)$:
{{begin-eqn}}
{{eqn | l = 0
      | o = <
      | r = b \int_0^1 p^{2 n + 1} e^{p x} \map f x \rd x
      | c = 
}}
{{eqn | o = <
      | r = \frac {b p^{2 n + 1} e^p} {n!}
      | c = 
}}
{{eqn | r = b p e^p \frac {\paren {p^2}^n e^p} {n!}
      | c = 
}}
{{end-eqn}}
The expression on the {{RHS}} tends to $0$ as $n$ tends to $\infty$.
Hence:
:$0 < a \, \map F 1 - b \, \map F 0 < 1$
for sufficiently large $n$.
But there exists no integer strictly between $0$ and $1$.
From this contradiction it follows that our original assumption, that is, that $e^r$ is rational, must have been false.
{{qed}}
Theorem: Rational Points on Graph of Exponential Function

Consider the graph $f$ of the exponential function in the real Cartesian plane $\R^2$:
:$f := \set {\tuple {x, y} \in \R^2: y = e^x}$
The only rational point of $f$ is $\tuple {0, 1}$.

Proof:
From Exponential of Rational Number is Irrational:
:$r \in \Q_{\ne 0} \implies e^r \in \R - \Q$
Thus, apart from the point $\tuple {0, 1}$, when $x$ is rational, $e^x$ is not.
Hence the result.
{{qed}}
Theorem: Rational Points on Graph of Logarithm Function

Consider the graph of the logarithm function in the real Cartesian plane $\R^2$:
:$f := \set {\tuple {x, y} \in \R^2: y = \ln x}$
The only rational point of $f$ is $\tuple {1, 0}$.

Proof:
Consider the graph of the exponential function in the real Cartesian plane $\R^2$:
:$g := \set {\tuple {x, y} \in \R^2: y = e^x}$
From Rational Points on Graph of Exponential Function, the only rational point of $g$ is $\tuple {0, 1}$.
By definition of the exponential function, $f$ and $g$ are inverses.
Thus:
:$\tuple {x, y} \in g \iff \tuple {y, x} \in f$
Thus for $\tuple {x, y} \in g$ to be rational, $\tuple {y, x} = \tuple {0, 1}$.
Hence the result.
{{qed}}