avewright/proofwiki-math huggingface dataset:
Theorem: One Sixth as Pandigital Fraction

There are $3$ ways $\dfrac 1 6$ can be expressed as a pandigital fraction:
:$\dfrac 1 6 = \dfrac {2943} {17658}$
:$\dfrac 1 6 = \dfrac {4653} {27918}$
:$\dfrac 1 6 = \dfrac {5697} {34182}$

Proof:
Can be verified by brute force.
Theorem: One Eighth as Pandigital Fraction

There are $46$ ways $\dfrac 1 8$ can be expressed as a pandigital fraction:
:$\dfrac 1 8 = \dfrac {3187} {25496}$
:$\dfrac 1 8 = \dfrac {4589} {36712}$
:$\dfrac 1 8 = \dfrac {4591} {36728}$
:$\dfrac 1 8 = \dfrac {4689} {37512}$
:$\dfrac 1 8 = \dfrac {4691} {37528}$
:$\dfrac 1 8 = \dfrac {4769} {38152}$
:$\dfrac 1 8 = \dfrac {5237} {41896}$
:$\dfrac 1 8 = \dfrac {5371} {42968}$
:$\dfrac 1 8 = \dfrac {5789} {46312}$
:$\dfrac 1 8 = \dfrac {5791} {46328}$
:$\dfrac 1 8 = \dfrac {5839} {46712}$
:$\dfrac 1 8 = \dfrac {5892} {47136}$
:$\dfrac 1 8 = \dfrac {5916} {47328}$
:$\dfrac 1 8 = \dfrac {5921} {47368}$
:$\dfrac 1 8 = \dfrac {6479} {51832}$
:$\dfrac 1 8 = \dfrac {6741} {53928}$
:$\dfrac 1 8 = \dfrac {6789} {54312}$
:$\dfrac 1 8 = \dfrac {6791} {54328}$
:$\dfrac 1 8 = \dfrac {6839} {54712}$
:$\dfrac 1 8 = \dfrac {7123} {56984}$
:$\dfrac 1 8 = \dfrac {7312} {58496}$
:$\dfrac 1 8 = \dfrac {7364} {58912}$
:$\dfrac 1 8 = \dfrac {7416} {59328}$
:$\dfrac 1 8 = \dfrac {7421} {59368}$
:$\dfrac 1 8 = \dfrac {7894} {63152}$
:$\dfrac 1 8 = \dfrac {7941} {63528}$
:$\dfrac 1 8 = \dfrac {8174} {65392}$
:$\dfrac 1 8 = \dfrac {8179} {65432}$
:$\dfrac 1 8 = \dfrac {8394} {67152}$
:$\dfrac 1 8 = \dfrac {8419} {67352}$
:$\dfrac 1 8 = \dfrac {8439} {67512}$
:$\dfrac 1 8 = \dfrac {8932} {71456}$
:$\dfrac 1 8 = \dfrac {8942} {71536}$
:$\dfrac 1 8 = \dfrac {8953} {71624}$
:$\dfrac 1 8 = \dfrac {8954} {71632}$
:$\dfrac 1 8 = \dfrac {9156} {73248}$
:$\dfrac 1 8 = \dfrac {9158} {73264}$
:$\dfrac 1 8 = \dfrac {9182} {73456}$
:$\dfrac 1 8 = \dfrac {9316} {74528}$
:$\dfrac 1 8 = \dfrac {9321} {74568}$
:$\dfrac 1 8 = \dfrac {9352} {74816}$
:$\dfrac 1 8 = \dfrac {9416} {75328}$
:$\dfrac 1 8 = \dfrac {9421} {75368}$
:$\dfrac 1 8 = \dfrac {9523} {76184}$
:$\dfrac 1 8 = \dfrac {9531} {76248}$
:$\dfrac 1 8 = \dfrac {9541} {76328}$

Proof:
Can be verified by brute force.
Theorem: One Ninth as Pandigital Fraction

There are $3$ ways $\dfrac 1 9$ can be expressed as a pandigital fraction:
{{begin-eqn}}
{{eqn | l = \dfrac 1 9
      | r = \dfrac {6381} {57429}
}}
{{eqn | l = \dfrac 1 9
      | r = \dfrac {6471} {58239}
}}
{{eqn | l = \dfrac 1 9
      | r = \dfrac {8361} {75249}
}}
{{end-eqn}}

Proof:
Can be verified by brute force.
Theorem: Four Fifths as Pandigital Fraction

The fraction $\dfrac 4 5$ can be expressed as a pandigital fraction in the following interesting way:
:$\dfrac 4 5 = \dfrac {9876} {12 \, 345}$

Proof:
Can be found by brute force.
Theorem: Probability of Two Random Integers having no Common Divisor

Let $a$ and $b$ be integers chosen at random.
The probability that $a$ and $b$ are coprime is given by:
:$\map \Pr {a \perp b} = \dfrac 1 {\map \zeta 2} = \dfrac 6 {\pi^2}$
where $\zeta$ denotes the zeta function.
The decimal expansion of $\dfrac 1 {\map \zeta 2}$ starts:
:$\dfrac 1 {\map \zeta 2} = 0 \cdotp 60792 \, 71018 \, 54026 \, 6 \ldots$
{{OEIS|A059956}}

Proof:
Let $a$ and $b$ be two integers chosen at random.
For $a$ and $b$ to be coprime, it is necessary and sufficient that no prime number divides both of them.
The probability that any particular integer is divisible by a prime number $p$ is $\dfrac 1 p$.
Hence the probability that both $a$ and $b$ are divisible by $p$ is $\dfrac 1 {p^2}$.
The probability that either $a$ or $b$ or both is not divisible by $p$ is therefore $1 - \dfrac 1 {p^2}$.
Whether or not $a$ is divisible by $p$ or divisible by another prime number $q$ is independent of both $p$ and $q$.
Thus by the Product Rule for Probabilities, the probability that $a$ and $b$ are not both divisible by either $p$ or $q$ is $\paren {1 - \dfrac 1 {p^2} } \paren {1 - \dfrac 1 {q^2} }$.
This independence extends to all prime numbers.
That is, the probability that $a$ and $b$ are not both divisible by any prime number is equal to the product of $1 - \dfrac 1 {p^2}$ over all prime numbers:
:$\map \Pr {a \perp b} = \ds \prod_{\text {$p$ prime} } \paren {1 - \dfrac 1 {p^2} }$
From Sum of Reciprocals of Powers as Euler Product:
:$\ds \map \zeta s = \prod_p \frac 1 {1 - p^{-s} }$
from which:
:$\ds \dfrac 1 {\map \zeta 2} = \prod_{\text {$p$ prime} } \paren {1 - \dfrac 1 {p^2} }$
where $\map \zeta 2$ is the Riemann $\zeta$ (zeta) function evaluated at $2$.
The result follows from Riemann Zeta Function of 2.
{{qed}}
Theorem: Probability of Random Integer being Square-Free

Let $a$ be an integer chosen at random.
The probability that $a$ is square-free is given by:
:$\map \Pr {\neg \exists b \in \Z: b^2 \divides a} = \dfrac 1 {\map \zeta 2} = \dfrac 6 {\pi^2}$
where $\zeta$ denotes the zeta function.
The decimal expansion of $\dfrac 1 {\map \zeta 2}$ starts:
:$\dfrac 1 {\map \zeta 2} = 0 \cdotp 60792 \, 71018 \, 54026 \, 6 \ldots$
{{OEIS|A059956}}

Proof:
Let $a$ be an integer chosen at random.
For $a$ to be square-free, it is necessary and sufficient that for all prime numbers $p$, it is not the case that $p^2$ is a  divisor of $a$.
The probability that any particular integer is divisible by $p^2$ is $\dfrac 1 {p^2}$.
The probability that $a$ is not divisible by $p^2$ is therefore $1 - \dfrac 1 {p^2}$.
Whether or not $a$ is divisible by $p^2$ or divisible by $q^2$ for another prime number $q$ is independent of both $p$ and $q$.
Thus by the Product Rule for Probabilities, the probability that $a$ is not divisible by either $p^2$ or $q^2$ is $\paren {1 - \dfrac 1 {p^2} } \paren {1 - \dfrac 1 {q^2} }$.
This independence extends to all prime numbers.
That is, the probability that $a$ is not divisible by the square of any prime number is equal to the product of $1 - \dfrac 1 {p^2}$ over all prime numbers:
:$\map \Pr {\neg \exists b \in \Z: b^2 \divides a} = \ds \prod_{\text {$p$ prime} } \paren {1 - \dfrac 1 {p^2} }$
From Sum of Reciprocals of Powers as Euler Product:
:$\ds \map \zeta s = \prod_p \frac 1 {1 - p^{-s} }$
from which:
:$\ds \dfrac 1 {\map \zeta 2} = \prod_{\text {$p$ prime} } \paren {1 - \dfrac 1 {p^2} }$
where $\map \zeta 2$ is the Riemann $\zeta$ (zeta) function evaluated at $2$.
The result follows from Riemann Zeta Function of 2.
{{qed}}
Theorem: Prime Ideal is Prime Element

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a lattice.
Let $I$ be an ideal in $L$.
Then:
:$I$ is a prime ideal
{{iff}}:
:$I$ is a prime element in $\struct {\map {\mathit {Ids} } L, \precsim}$
where:
:$\map {\mathit {Ids} } L$ denotes the set of all ideals in $L$
:$\mathord \precsim := \mathord \subseteq \restriction_{\map {\mathit {Ids} } L \times \map {\mathit {Ids} } L}$

Proof:
=== Sufficient Condition ===
Let $I$ be a prime ideal.
Let $x, y \in \map {\mathit {Ids} } L$ such that
:$x \wedge y \precsim I$
By definition of $\precsim$:
:$x \wedge y \subseteq I$
By Meet is Intersection in Set of Ideals:
:$x \cap y \subseteq I$
{{AimForCont}}:
:$x \not \precsim I$ and $y \not \precsim I$
By definition of $\precsim$:
$x \nsubseteq I$ and $y \nsubseteq I$
By definition of subset:
:$\exists a \in x: a \notin I$
and
:$\exists b \in y: b \notin I$
By Meet Precedes Operands:
:$a \wedge b \preceq a$ and $a \wedge b \preceq b$
By definition lower section:
:$a \wedge b \in x$ and $a \wedge b \in y$
By definitions subset and intersection:
:$a \wedge b \in I$
By Characterization of Prime Ideal:
:$a \in I$ or $b \in I$
This contradicts $a \notin I$ and $b \notin I$
Hence the assumption:
:$x \not \precsim I$ and $y \not \precsim I$
was false.
{{qed|lemma}}
Theorem: Probability of Three Random Integers having no Common Divisor

Let $a, b$ and $c$ be integers chosen at random.
The probability that $a, b$ and $c$ have no common divisor:
:$\map \Pr {\map \perp {a, b, c} } = \dfrac 1 {\map \zeta 3}$
where $\zeta$ denotes the zeta function:
:$\map \zeta 3 = \dfrac 1 {1^3} + \dfrac 1 {2^3} + \dfrac 1 {3^3} + \dfrac 1 {4^3} + \cdots$
The decimal expansion of $\dfrac 1 {\map \zeta 3}$ starts:
:$\dfrac 1 {\map \zeta 3} = 0 \cdotp 83190 \, 73725 \, 80707 \ldots$
{{OEIS|A088453}}

Proof:
Let $a$, $b$ and $c$ be three integers chosen at random.
For $a$, $b$ and $c$ to be coprime, it is necessary and sufficient that no prime number divides all of them.
The probability that any particular integer is divisible by a prime number $p$ is $\dfrac 1 p$.
Hence the probability that $a$, $b$ and $c$ are divisible by $p$ is $\dfrac 1 {p^3}$.
The probability that at least one of $a$, $b$ and $c$ is not divisible by $p$ is therefore $1 - \dfrac 1 {p^3}$.
Whether or not $a$ is divisible by $p$ or divisible by another prime number $q$ is independent of both $p$ and $q$.
Thus by the Product Rule for Probabilities, the probability that $a$, $b$ and $c$ are not all divisible by either $p$ or $q$ is $\paren {1 - \dfrac 1 {p^3} } \paren {1 - \dfrac 1 {q^3} }$.
This independence extends to all prime numbers.
That is, the probability that $a$, $b$ and $c$ are not all divisible by any prime number is equal to the product of $1 - \dfrac 1 {p^3}$ over all prime numbers:
:$\map \Pr {\map \perp {a, b, c} } = \ds \prod_{\text {$p$ prime} } \paren {1 - \dfrac 1 {p^3} }$
From Sum of Reciprocals of Powers as Euler Product:
:$\ds \map \zeta s = \prod_p \frac 1 {1 - p^{-s} }$
from which:
:$\ds \dfrac 1 {\map \zeta 3} = \prod_{\text {$p$ prime} } \paren {1 - \dfrac 1 {p^3} }$
where $\map \zeta 3$ is the Riemann $\zeta$ (zeta) function evaluated at $3$.
The result follows.
{{qed}}
Theorem: Densest Packing of Identical Circles

The densest packing of identical circles in the plane obtains a density of $\dfrac \pi {2 \sqrt 3} = \dfrac \pi {\sqrt {12} }$:
:$\dfrac \pi {2 \sqrt 3} = 0 \cdotp 90689 \, 96821 \ldots$
{{OEIS|A093766}}
This happens when they are packed together in a hexagonal array, with each circle touching $6$ others.

Proof:
{{ProofWanted|It remains to be proved that the hexagonal packing is in fact the densest that can be achieved.}}
Consider the rectangular area $ABCD$ of the densest packing of circles.
:300px
Let the radius of one circle be $1$.
The length $AB$ is $2$.
The length $AC$ is $2 \sqrt 3$.
Thus, from Area of Rectangle, the area of $\Box ABCD$ is $4 \sqrt 3$.
Within $ABCD$ there is one complete circle and one quarter of each of $4$ other circles.
That makes a total of $2$ circles.
Thus, from Area of Circle, the area of $ABCD$ which is inside a circle is $2 \pi$.
So the density is:
{{begin-eqn}}
{{eqn | l = \dfrac {\text {Area of Circles} } {\text {Area of Rectangle} }
      | r = \dfrac {2 \pi} {4 \sqrt 3}
      | c = 
}}
{{eqn | r = \dfrac {\pi} {2 \sqrt 3}
      | c = 
}}
{{eqn | r = \dfrac {\pi} {12}
      | c = 
}}
{{end-eqn}}
as required.
Theorem: Anning's Theorem

In any base greater than $1$, the fraction:
:$\dfrac {101 \, 010 \, 101} {110 \, 010 \, 011}$
has the property that if the two $1$'s in the center of the numerator and the denominator are replaced by the same odd number of $1$'s, the value of the fraction remains the same.
For example:
:$\dfrac {101 \, 010 \, 101} {110 \, 010 \, 011} = \dfrac {1 \, 010 \, 111 \, 110 \, 101} {1 \, 100 \, 111 \, 110 \, 011} = \dfrac {9091} {9901}$ (in base $10$).

Proof:
Let $b$ be the base in question.
Let $F = \dfrac {101 \, 010 \, 101} {110 \, 010 \, 011}$.
Then:
:$F = \dfrac {1 + b^2 + b^4 + b^6 + b^8} {1 + b + b^4 + b^7 + b^8}$
It is necessary to prove that for all $k \in \Z_{>0}$:
:$F = \dfrac {1 + b^2 + b^4 + b^5 + \cdots + b^{2 k + 2} + b^{2 k + 4} + b^{2 k + 6} } {1 + b + b^4 + b^5 + \cdots + b^{2 k + 2} + b^{2 k + 5} + b^{2 k + 6} }$
This is done by:
: multiplying the numerator of one by the denominator of the other
and then:
: multiplying the denominator of one by the numerator of the other
and checking that they are equal.
Thus we proceed:
{{begin-eqn}}
{{eqn | o = 
      | r = 1 + b^2 + b^4 + b^6 + b^8
      | c = 
}}
{{eqn | o = 
      | ro= \times
      | r = 1 + b + b^4 + b^5 + \cdots + b^{2 k + 2} + b^{2 k + 5} + b^{2 k + 6}
      | c = 
}}
{{eqn | o = =
      | r = 1 + b + b^4 + b^5 + \cdots + b^{2 k + 2} + b^{2 k + 5} + b^{2 k + 6}
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = b^2 + b^3 + b^6 + b^7 + \cdots + b^{2 k + 4} + b^{2 k + 7} + b^{2 k + 8}
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = b^4 + b^5 + b^8 + b^9 + \cdots + b^{2 k + 6} + b^{2 k + 9} + b^{2 k + 10}
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = b^6 + b^7 + b^{10} + b^{11} + \cdots + b^{2 k + 8} + b^{2 k + 11} + b^{2 k + 12}
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = b^8 + b^9 + b^{12} + b^{13} + \cdots + b^{2 k + 10} + b^{2 k + 13} + b^{2 k + 14}
      | c = 
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | o = 
      | r = 1 + b + b^4 + b^7 + b^8
      | c = 
}}
{{eqn | o = 
      | ro= \times
      | r = 1 + b^2 + b^4 + b^5 + \cdots + b^{2 k + 2} + b^{2 k + 4} + b^{2 k + 6}
      | c = 
}}
{{eqn | o = =
      | r = 1 + b^2 + b^4 + b^5 + \cdots + b^{2 k + 2} + b^{2 k + 4} + b^{2 k + 6}
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = b + b^3 + b^5 + b^6 + \cdots + b^{2 k + 3} + b^{2 k + 5} + b^{2 k + 7}
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = b^4 + b^6 + b^8 + b^9 + \cdots + b^{2 k + 6} + b^{2 k + 8} + b^{2 k + 10}
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = b^7 + b^9 + b^{11} + b^{12} + \cdots + b^{2 k + 9} + b^{2 k + 11} + b^{2 k + 13}
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = b^8 + b^{10} + b^{12} + b^{13} + \cdots + b^{2 k + 10} + b^{2 k + 12} + b^{2 k + 14}
      | c = 
}}
{{end-eqn}}
Equality can be demonstrated.
{{qed}}
{{Namedfor|Norman Herbert Anning|cat = Anning}}
Theorem: Meet is Intersection in Set of Ideals

Let $\mathscr S = \struct {S, \wedge, \preceq}$ be a meet semilattice.
Let $\map {\mathit {Ids} } {\mathscr S}$ be the set of all ideals in $\mathscr S$.
Let $P = \struct {\map {\mathit {Ids} } {\mathscr S}, \precsim}$ be an ordered set where $\mathord \precsim = \mathord \subseteq \restriction_{\map {\mathit {Ids} } {\mathscr S} \times \map {\mathit {Ids} } {\mathscr S} }$
Let $I_1, I_2$ be ideals in $\mathscr S$.
Then
:$I_1 \wedge_P I_2 = I_1 \cap I_2$

Proof:
By Intersection of Semilattice Ideals is Ideal:
:$I_1 \cap I_2 \in \map {\mathit {Ids} } {\mathscr S}$
We will prove that
:$I_1 \cap I_2$ is lower bound for $\set {I_1, I_2}$
Let $x \in \set {I_1, I_2}$.
Then by definition of unordered tuple:
:$x = I_1$ or $x = I_2$
By Intersection is Subset
:$I_1 \cap I_2 \subseteq x$
Thus by definition of $\precsim$:
:$I_1 \cap I_2 \precsim x$
{{qed|lemma}}
We will prove that
:$\forall I \in \map {\mathit {Ids} } {\mathscr S}: I$ is lower bound for $\set {I_1, I_2} \implies I \precsim I_1 \cap I_2$
Let $I \in \map {\mathit {Ids} } {\mathscr S}$ such that
:$I$ is lower bound for $\set {I_1, I_2}$
By definition of lower bound:
:$I \precsim I_1$ and $I \precsim I_2$
By definition of $\precsim$:
:$I \subseteq I_1$ and $I \subseteq I_2$
By Intersection is Largest Subset:
:$I \subseteq I_1 \cap I_2$
Thus by definition of $\precsim$
:$I \precsim I_1 \cap I_2$
{{qed|lemma}}
By definition of infimum:
:$\inf \set {I_1, I_2} = I_1 \cap I_2$
Hence by definition of meet:
:$I_1 \wedge I_2 = I_1 \cap I_2$
{{qed}}
Theorem: Characterization of Prime Ideal by Finite Infima

Let $L = \struct {S, \wedge, \preceq}$ be a meet semilattice.
Let $I$ be an ideal in $L$.
Then
:$I$ is a prime ideal
{{iff}}
:for all non-empty finite subset $A$ of $S: \paren {\inf A \in I \implies \exists a \in A: a \in I}$

Proof:
=== Sufficient Condition ===
Let $I$ be a prime ideal.
Define:
:$\map P X: \equiv X \ne \O \land \inf X \in I \implies \exists x \in X: x \in I$
where $X$ is subset of $S$.
Let $A$ be a non-empty finite subset of $S$.
By definition of empty set:
:$\map P \O$
We will prove that:
:$\forall x \in A, B \subseteq A: \map P B \implies \map P {B \cup \set x}$
Let $x \in A, B \subseteq A$ such that:
:$\map P B$
This will be used as an induction hypothesis.
Assume that:
:$B \cup \set x \ne \O$ and $\map \inf {B \cup \set x} \in I$
;Case $B = \O$
By Union with Empty Set:
:$B \cup \set x = \set x$
By Infimum of Singleton:
:$\inf \set x = x$
By definition of singleton:
:$x \in \set x$
Thus
:$\exists a \in B \cup \set x: a \in I$
{{qed|lemma}}
;Case $B \ne \O$
By Subset of Finite Set is Finite:
:$B$ is finite.
By Existence of Non-Empty Finite Infima in Meet Semilattice:
:$B$ admits an infimum.
By Infimum of Singleton:
:$\set x$ admits an infimum.
{{begin-eqn}}
{{eqn | l = \map \inf {B \cup \set x}
      | r = \map \inf {\bigcup \set {B, \set x} }
      | c = {{Defof|Set Union}}
}}
{{eqn | r = \inf \set {\inf B, x}
      | c = Infimum of Infima
}}
{{eqn | r = \paren {\inf B} \wedge x
      | c = {{Defof|Meet (Order Theory)|Meet}}
}}
{{end-eqn}}
By Characterization of Prime Ideal:
:$\inf B \in I$ or $x \in I$
;Case $\inf B \in I$
By the induction hypothesis:
:$\exists a \in B: a \in I$
By definition of union:
:$a \in B \cup \set x$
Thus:
:$\exists a \in B \cup \set x: a \in I$
{{qed|lemma}}
;Case $x \in I$:
By definition of union:
:$x \in B \cup \set x$
Thus
:$\exists a \in B \cup \set x: a \in I$
{{qed|lemma}}
By Induction of Finite Set:
:$\map P A$
Thus the result.
{{qed|lemma}}
Theorem: Unordered Pair is Finite

Let $x, y$ be arbitrary.
Then $\set {x, y}$ is finite.

Proof:
By Union of Disjoint Singletons is Doubleton:
:$\set {x, y} = \set x \cup \set y$
By Singleton is Finite:
:$\set x$ and $\set y$ are finite.
Thus by Union of Finite Sets is Finite:
:$\set {x, y}$ is finite.
{{qed}}
Theorem: Length of Diagonal of Unit Square

The length of a diagonal of a square of side length $1$ is $\sqrt 2$) (the square root of $2$).

Proof:
:300px
Two adjacent sides $AB$, $BC$ and the diagonal $AC$ of square $ABCD$ form a right triangle.
The hypotenuse of triangle $\triangle ABC$ can be found by using Pythagoras's Theorem:
:$AC^2 = AB^2 + BC^2$
from which:
:$AC^2 = 2$
and so:
:$AC = \sqrt 2$
{{qed}}
Theorem: Sequence of Best Rational Approximations to Square Root of 2

A sequence of best rational approximations to the square root of $2$ starts:
:$\dfrac 1 1, \dfrac 3 2, \dfrac 7 5, \dfrac {17} {12}, \dfrac {41} {29}, \dfrac {99} {70}, \dfrac {239} {169}, \dfrac {577} {408}, \ldots$
where:
:the numerators are half of the Pell-Lucas numbers, $\dfrac 1 2 Q_n$
:the denominators are the Pell numbers $P_n$
starting from $\dfrac {\tfrac12 Q_1} {P_1}$.
{{OEIS-Numerators|A001333}}
{{OEIS-Denominators|A000129}}

Proof:
Let $\tuple {a_0, a_1, \ldots}$ be the continued fraction expansion of $\sqrt 2$.
By Continued Fraction Expansion of Root 2:
:$\sqrt 2 = \sqbrk {1, \sequence 2} = \sqbrk {1, 2, 2, 2, \ldots}$
From Convergents are Best Approximations, the convergents of $\sqbrk {1, \sequence 2}$ are the best rational approximations of $\sqrt 2$.
Let $\sequence {p_n}_{n \mathop \ge 0}$ and $\sequence {q_n}_{n \mathop \ge 0}$ be the numerators and denominators of the continued fraction expansion of $\sqrt 2$.
Then $\dfrac {p_n} {q_n}$ is the $n$th convergent of $\sqbrk {1, \sequence 2}$.
By Convergents of Simple Continued Fraction are Rationals in Canonical Form, $p_n$ and $q_n$ are coprime for all $n \ge 0$.
It remains to show that for all $n \ge 1$:
:$Q_n = 2 p_{n - 1}$
:$P_n = q_{n - 1}$
It is sufficient to prove that they satisfy the same recurrence relation.
By definition:
{{begin-eqn}}
{{eqn | l = p_0
      | r = a_0
}}
{{eqn | r = 1
}}
{{eqn | l = q_0
      | r = 1
}}
{{end-eqn}}
so that:
:$\tuple {Q_1, P_1} = \tuple {2, 1} = \tuple {2 p_0, q_0}$
{{begin-eqn}}
{{eqn | l = p_1
      | r = a_0 a_1 + 1
}}
{{eqn | r = 1 \times 2 + 1
}}
{{eqn | r = 3
}}
{{eqn | l = q_1
      | r = a_1
}}
{{eqn | r = 2
}}
{{end-eqn}}
so that:
:$\tuple {Q_2, P_2} = \tuple {6, 2} = \tuple {2 p_1, q_1}$
{{begin-eqn}}
{{eqn | l = p_k
      | r = a_k p_{k - 1} + p_{k - 2}
}}
{{eqn | r = 2 p_{k - 1} + p_{k - 2}
}}
{{eqn | l = q_k
      | r = a_k q_{k - 1} + q_{k - 2}
}}
{{eqn | r = 2 q_{k - 1} + q_{k - 2}
}}
{{end-eqn}}
The result follows by definition of Pell numbers and Pell-Lucas numbers.
{{qed}}
Theorem: Difference between Adjacent Convergents of Simple Continued Fraction

Then for $k \ge 1$:
:$p_k q_{k - 1} - p_{k - 1} q_k = \paren {-1}^{k + 1}$
That is:
:$C_k - C_{k - 1} = \dfrac {p_k} {q_k} - \dfrac {p_{k - 1} } {q_{k - 1} } = \dfrac {\paren {-1}^{k + 1} } {q_k q_{k - 1} }$

Proof:
Proof by induction:
For all $n \in \Z: n \ge 2$, let $\map P n$ be the proposition:
:$p_n q_{n - 1} - p_{n - 1} q_n = \paren {-1}^{n + 1}$
Theorem: Difference between Adjacent Convergents But One of Simple Continued Fraction

For $k \ge 2$:
:$p_k q_{k - 2} - p_{k - 2} q_k = \paren {-1}^k a_k$
That is:
:$C_k - C_{k-2} = \dfrac {p_k} {q_k} - \dfrac {p_{k - 2} } {q_{k - 2} } = \dfrac {\paren {-1}^k a_k} {q_k q_{k - 2} }$

Proof:
Let $k \ge 2$.
{{begin-eqn}}
{{eqn | l = p_k q_{k - 2} - p_{k - 2} q_k
      | r = \paren {a_k p_{k - 1} + p_{k - 2} } q_{k - 2} - p_{k - 2} \paren {a_k q_{k - 1} + q_{k - 2} }
      | c = {{Defof|Numerators and Denominators of Continued Fraction}}
}}
{{eqn | r = a_k \paren {p_{k - 1} q_{k - 2} - p_{k - 2} q_{k - 1} }
      | c = 
}}
{{eqn | r = a_k \paren {-1}^k
      | c = Difference between Adjacent Convergents of Simple Continued Fraction
}}
{{end-eqn}}
{{qed}}
Category:Simple Continued Fractions
34jnwej6sjfq1u5zmxus7vezcwn8vef
Theorem: Convergents of Simple Continued Fraction are Rationals in Canonical Form

For all $k \ge 1$, $\dfrac {p_k} {q_k}$ is in canonical form:
:$p_k$ and $q_k$ are coprime
:$q_k > 0$.

Proof:
Let $k \ge 1$.
Let $d = \gcd \set {p_k, q_k}$.
From Common Divisor Divides Integer Combination:
:$p_k q_{k - 1} - p_{k - 1} q_k$ is a multiple of $d$.
From Difference between Adjacent Convergents of Simple Continued Fraction:
:$d \divides \paren {-1}^{k + 1}$
where $\divides$ denotes divisibility.
It follows that:
:$d = 1$
By:
:$q_0 = 1$
:Denominators of Simple Continued Fraction are Strictly Increasing
It follows that $q_k > 0$ for all $k \ge 0$.
{{qed}}
Category:Simple Continued Fractions
3mhh3l6japk1khrvp1r7rv242x5k7p1
Theorem: Characterization of Prime Filter by Finite Suprema

Let $L = \struct {S, \vee, \preceq}$ be a join semilattice.
Let $F$ be a filter in $L$.
Then
:$F$ is a prime filter
{{iff}}:
:for all non-empty finite subset $A$ of $S: \paren {\sup A \in F \implies \exists a \in A: a \in F}$

Proof:
=== Sufficient Condition ===
Let $F$ be a prime ideal.
Define $\map \PP X: \equiv X \ne \O \land \sup X \in F \implies \exists x \in X: x \in F$
where $X$ is subset of $S$.
Let $A$ be a non-empty finite subset of $S$.
By definition of empty set:
:$\map \PP \O$
We will prove that:
:$\forall x \in A, B \subseteq A: \map \PP B \implies \map \PP {B \cup \set x}$
Let $x \in A, B \subseteq A$ such that:
:$\map \PP B$ (Induction Hypothesis)
Assume that:
:$B \cup \set x \ne \O$ and $\map \sup {B \cup \set x} \in F$
Case $B = \O$:
By Union with Empty Set:
:$B \cup \set x = \set x$
By Supremum of Singleton:
:$\sup \set x = x$
By definition of singleton:
:$x \in \set x$
Thus
:$\exists a \in B \cup \set x: a \in F$
{{qed|lemma}}
Case $B \ne \O$:
By Subset of Finite Set is Finite:
:$B$ is finite.
By Existence of Non-Empty Finite Suprema in Join Semilattice:
:$B$ admits a supremum.
By Supremum of Singleton:
:$\set x$ admits a supremum.
{{begin-eqn}}
{{eqn | l = \map \sup {B \cup \set x}
      | r = \map \sup {\bigcup \set {B, \set x} }
      | c = {{Defof|Set Union}}
}}
{{eqn | r = \sup \set {\sup B, x}
      | c = Supremum of Suprema:
}}
{{eqn | r = \paren {\sup B} \vee x
      | c = {{Defof|Join (Order Theory)}}
}}
{{end-eqn}}
By definition of prime filter:
:$\sup B \in F$ or $x \in F$
Case $\sup B \in F$:
By Induction Hypothesis:
:$\exists a \in B: a \in F$
By definition of union:
:$a \in B \cup \set x$
Thus:
:$\exists a \in B \cup \set x: a \in F$
{{qed|lemma}}
Case $x \in F$:
By definition of union:
:$x \in B \cup \set x$
Thus:
:$\exists a \in B \cup \set x: a \in F$
{{qed|lemma}}
By Induction of Finite Set:
:$\map \PP A$
Thus the result.
{{qed|lemma}}
Theorem: Dual of Preordered Set is Preordered Set

Let $P = \struct {S, \preceq}$ be a preordered set.
Then dual of $P$, $P^{-1} = \struct {S, \succeq}$ is also a preordered set.
{{finish|Dual Ordered Set $\ne$ Dual Preordered Set}}

Proof:
By Inverse of Reflexive Relation is Reflexive:
:$\succeq$ is reflexive.
By Inverse of Transitive Relation is Transitive:
:$\succeq$ is transitive.
Hence $\succeq$ is a preordering.
{{qed}}