avewright/proofwiki-math huggingface dataset:
Theorem: Dual Ordered Set is Ordered Set

Let $P = \struct {S, \preceq}$ be an ordered set.
Then its dual, $P^{-1} = \struct {S, \succeq}$, is also an ordered set.

Proof:
Immediate from Dual Ordering is Ordering.
{{qed}}
Theorem: Value of Finite Continued Fraction equals Numerator Divided by Denominator

Let $F$ be a field.
Let $\tuple {a_0, a_1, \ldots, a_n}$ be a finite continued fraction of length $n \ge 0$.
Let $p_n$ and $q_n$ be its $n$th numerator and denominator.
Then the value $\sqbrk {a_0, a_1, \ldots, a_n}$ equals $\dfrac {p_n} {q_n}$.

Proof:
We will use a proof by induction on the length $n$.
For all $n \in \Z_{>0}$, let $\map P n$ be the proposition:
:$\sqbrk {a_0, a_1, \ldots, a_n} = \dfrac {p_n} {q_n}$
Theorem: Simple Infinite Continued Fraction Converges

Let $C = (a_0, a_1, \ldots)$ be a simple infinite continued fraction in $\R$.
Then $C$ converges.

Proof:
We need to show that for any SICF its sequence of convergents $\sequence {C_n}$ always tends to a limit.
Let $\epsilon > 0$.
For $m > n \ge \max \set {5, \dfrac 1 \epsilon}$:
{{begin-eqn}}
{{eqn | l = \size {C_m - C_n}
      | o = \le
      | r = \size {C_m - C_{m - 1} } + \cdots + \size {C_{n + 1} - C_n}
      | c = Triangle Inequality
}}
{{eqn | r = \frac 1 {q_m q_{m - 1} } + \cdots + \frac 1 {q_{n + 1} q_n}
      | c = Difference between Adjacent Convergents of Simple Continued Fraction
}}
{{eqn | o = <
      | r = \frac 1 {m \paren {m - 1} } + \cdots + \frac 1 {\paren {n + 1} n}
      | c = Lower Bounds for Denominators of Simple Continued Fraction
}}
{{eqn | r = \sum_{k \mathop = n}^{m - 1} \frac 1 {k \paren {k + 1} }
}}
{{eqn | r = \sum_{k \mathop = n}^{m - 1} \paren {\frac 1 k - \frac 1 {k + 1} }
}}
{{eqn | r = \frac 1 n - \frac 1 m
      | c = Telescoping Series: Example 1
}}
{{eqn | o = <
      | r = \frac 1 n
}}
{{eqn | o = \le
      | r = \epsilon
}}
{{end-eqn}}
So $\sequence {C_n}$ is indeed a Cauchy sequence.
Hence the result.
{{qed}}
Theorem: Bound for Difference of Irrational Number with Convergent

Let $x$ be an irrational number.
Let $\sequence {C_n}$ be the sequence of convergents of the continued fraction expansion of $x$.
Then $\forall n \ge 1$:
:$C_n < x < C_{n + 1}$ or $C_{n + 1} < x < C_n$
:$\size {x - C_n} < \dfrac 1 {q_n q_{n + 1} }$

Proof:
{{questionable|this needs Correspondence between Irrational Numbers and Simple Infinite Continued Fractions}}
Immediate.
Note that:
:$\size {x - C_n} < \size {C_{n + 1} - C_n} = \dfrac 1 {q_n q_{n + 1} }$
{{qed}}
Category:Continued Fractions
3uolekaum9vp63qh9xj7w2yks1jnw2a
Theorem: Continued Fraction Identities/First/Infinite

Let $\left[{a_0, a_1, a_2, \ldots}\right]$ be a simple infinite continued fraction.
Then:
:$\left[{a_1, a_2, a_3, \ldots}\right] = a_1 + \dfrac 1 {\left[{a_2, a_3, \ldots}\right]}$

Proof:
{{proof wanted|use continuity}}
{{Qed}}
Category:Continued Fractions
5n4u82kpalt0upokwg3op45qyptfyp2
Theorem: Relation between Adjacent Best Rational Approximations to Root 2

Consider the Sequence of Best Rational Approximations to Square Root of 2:
:$\sequence S := \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$
Let $\dfrac {p_n} {q_n}$ and $\dfrac {p_{n + 1} } {q_{n + 1} }$ be adjacent terms of $\sequence S$.
Then:
:$\dfrac {p_{n + 1} } {q_{n + 1} } = \dfrac {p_n + 2 q_n} {p_n + q_n}$

Proof:
The proof proceeds by induction.
For all $n \in \Z_{> 0}$, let $\map P n$ be the proposition:
:$\dfrac {p_{n + 1} } {q_{n + 1} } = \dfrac {p_n + 2 q_n} {p_n + q_n}$
Theorem: Parity of Pell Numbers

Consider the Pell numbers $P_0, P_1, P_2, \ldots$
:$0, 1, 2, 5, 12, 29, \ldots$
$P_n$ has the same parity as $n$.
That is:
:if $n$ is odd then $P_n$ is odd
:if $n$ is even then $P_n$ is even.

Proof:
The proof proceeds by strong induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$P_n$ has the same parity as $n$.
Theorem: Parity of Best Rational Approximations to Root 2

Consider the Sequence of Best Rational Approximations to Square Root of 2:
:$\sequence S := \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 $S_1 := \dfrac 1 1$.
The numerators of the terms of $\sequence S$ are all odd.
For all $n$, the parity of the denominator of term $S_n$ is the same as the parity of $n$.

Proof:
First the parity of the numerators of the terms of $\sequence S$ is established.
Let $\dfrac {p_n} {q_n}$ be a general term of $\sequence S$.
By Relation between Adjacent Best Rational Approximations to Root 2:
:$p_{n + 1} = p_n + 2 q_n$
Thus if $p_n$ is odd then so is $p_{n + 1}$.
But $p_1 = 1$ is odd.
So $p_n$ is odd for all $n$, by Principle of Mathematical Induction.
The denominators are the Pell numbers.
The result follows from Parity of Pell Numbers.
{{qed}}
Category:Square Root of 2
i9dhdw5j9ztimw3f2vzovtljpv3jeui
Theorem: Best Rational Approximations to Root 2 generate Pythagorean Triples

Consider the Sequence of Best Rational Approximations to Square Root of 2:
:$\sequence S := \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$
Every odd term of $\sequence S$ can be expressed as:
:$\dfrac {2 a + 1} b$
such that:
:$a^2 + \paren {a + 1}^2 = b^2$

Proof:
From Parity of Best Rational Approximations to Root 2:
:The numerators of the terms of $\sequence S$ are all odd.
:For all $n$, the parity of the denominator of term $S_n$ is the same as the parity of $n$.
Thus it follows that every other term of $\sequence S$ has a numerator and a denominator which are both odd.
This proof proceeds by induction.
=== Basis for the Induction ===
$\dfrac 1 1$ can be expressed as $\dfrac {2(0) + 1} 1$, and:
:$0^2 + \paren {0 + 1}^2 = 1^2$
=== Induction Hypothesis ===
This is our induction hypothesis:
The best rational approximation $\dfrac {p_k} {q_k}$ of $\sqrt 2$, when expressed as:
:$\dfrac {2 a + 1} b$
gives the relation:
:$a^2 + \paren {a + 1}^2 = b^2$
We need to show that the best rational approximation $\dfrac {p_{k + 2} } {q_{k + 2} }$ of $\sqrt 2$, when expressed as:
:$\dfrac {2 a' + 1} {b'}$
also give the relation:
:$a'^2 + \paren {a' + 1}^2 = b'^2$
=== Induction Step ===
This is our induction step:
From the induction hypothesis we have:
:$a = \dfrac {p_k - 1} 2, b = q_k$
and thus:
:$\paren {\dfrac {p_k - 1} 2}^2 + \paren {\dfrac {p_k - 1} 2 + 1}^2 = q_k^2$
Expanding, we have:
:$\dfrac {p_k^2} 2 + \dfrac 1 2 = q_k^2$
Now by Relation between Adjacent Best Rational Approximations to Root 2, we have:
:$\dfrac {p_{k + 1} } {q_{k + 1} } = \dfrac {p_k + 2 q_k} {p_k + q_k}$
We check that, via GCD with Remainder:
:$\gcd \set {p_k + 2 q_k, p_k + q_k} = \gcd \set {q_k, p_k + q_k} = \gcd \set {q_k, p_k} = 1$
Since both fractions are in canonical form and Canonical Form of Rational Number is Unique, we can write:
:$p_{k + 1} = p_k + 2 q_k$
:$q_{k + 1} = p_k + q_k$
Therefore:
:$p_{k + 2} = 3 p_k + 4 q_k$
:$q_{k + 2} = 2 p_k + 3 q_k$
We need to show that:
:$\paren {\dfrac {p_{k + 2} - 1} 2}^2 + \paren {\dfrac {p_{k + 2} - 1} 2 + 1}^2 = q_k^2$
or:
:$\dfrac {p_{k + 2}^2} 2 + \dfrac 1 2 = q_{k + 2}^2$
We have:
{{begin-eqn}}
{{eqn | l = \frac {p_{k + 2}^2} 2 + \frac 1 2
      | r = \frac {\paren{3 p_k + 4 q_k}^2} 2 + \frac 1 2
}}
{{eqn | r = \frac {9 p_k^2 + 24 p_k q_k + 16 q_k^2} 2 + \frac 1 2
      | c = Square of Sum
}}
{{eqn | r = \frac {p_k^2} 2 + \frac 1 2 + 4 p_k^2 + 12 p_k q_k + 8 q_k^2
}}
{{eqn | r = 4 p_k^2 + 12 p_k q_k + 9 q_k^2
}}
{{eqn | r = \paren {2 p_k + 3 q_k}^2
      | c = Square of Sum
}}
{{eqn | r = q_{k + 2}^2
}}
{{end-eqn}}
The result follows by induction.
{{qed}}
Theorem: Best Rational Approximations to Root 2 generate Pythagorean Triples

Consider the Sequence of Best Rational Approximations to Square Root of 2:
:$\sequence S := \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$
Every odd term of $\sequence S$ can be expressed as:
:$\dfrac {2 a + 1} b$
such that:
:$a^2 + \paren {a + 1}^2 = b^2$

Proof:
From Pell Number as Sum of Squares, we have:
:$P_{2 n + 1} = P_{n + 1}^2 + P_n^2$
Therefore:
{{begin-eqn}}
{{eqn | l = P_{2 n + 1}^2
      | r = \paren {P_{n + 1}^2 + P_n^2}^2
}}
{{eqn | r = P_{n + 1}^4 + 2 P_{n + 1}^2 P_n^2 + P_n^4
      | c = Square of Sum
}}
{{eqn | r = P_{n + 1}^4 + 2 P_{n + 1}^2 P_n^2 + P_n^4 + 2 P_{n + 1}^2 P_n^2 - 2 P_{n + 1}^2 P_n^2
      | c = adding zero
}}
{{eqn | r = P_{n + 1}^4 - 2 P_{n + 1}^2 P_n^2 + P_n^4 + 4 P_{n + 1}^2 P_n^2 
      | c = regrouping
}}
{{eqn | r = \paren {P_{n + 1}^2 - P_n^2}^2 + \paren {2 P_{n + 1} P_n}^2 
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Prime Ideal is Prime Filter in Dual Ordered Set

Let $P = \struct {S, \preceq}$ be a ordered set.
Let $X$ be a subset of $S$.
Then
:$X$ is a prime ideal of $P$
{{iff}}:
:$X$ is a prime filter of $P^{-1}$
where $P^{-1} = \struct {S, \succeq}$ denotes the dual of $P$.

Proof:
=== Sufficient Condition ===
Let $X$ be a prime ideal in $P$.
Then
:$X$ is an ideal of $P$.
:$S \setminus X$ is a filter of $P$.
by definition of a prime ideal.
By Ideal is Filter in Dual Ordered Set:
:$X$ is a filter of $P^{-1}$.
and by Filter is Ideal in Dual Ordered Set:
:$S \setminus X$ is an ideal of $P^{-1}$.
Hence $X$ is a prime filter of $P^{-1}$ by definition.
{{qed|lemma}}
Theorem: Ideal is Filter in Dual Ordered Set

Let $P = \struct {S, \preceq}$ be an ordered set.
Let $X$ be a subset of $S$.
Then
:$X$ is ideal in $P$
{{iff}}
:$X$ is filter in $P^{-1}$
where $P^{-1} = \struct {S, \succeq}$ denotes the dual of $P$.

Proof:
=== Sufficient Condition ===
Let $X$ be ideal in $P$.
By definition of ideal in ordered set:
:$X$ is non-empty directed lower.
By definition of directed:
:$\forall x, y \in X: \exists z \in X: x \preceq z \land y \preceq z$
Then
:$\forall x, y \in X: \exists z \in X: z \succeq x \land z \succeq y$
By definition
:$X$ is filtered in $P^{-1}$
By definition of lower section:
:$\forall x \in X, y \in S: y \preceq x \implies y \in X$
Then
:$\forall x \in X, y \in S: x \succeq y \implies y \in X$
By definition
:$X$ is an upper section in $P^{-1}$.
Thus by definition of filter in ordered set
:$X$ is a filter in $P^{-1}$.
{{qed|lemma}}
Theorem: Square Root of 2 as Sum of Egyptian Fractions

The square root of $2$ can be approximated by the following sequence of Egyptian fractions:
:$\sqrt 2 = 1 + \dfrac 1 3 + \dfrac 1 {13} + \dfrac 1 {253} + \dfrac 1 {218 \, 201} + \dfrac 1 {61 \, 323 \, 543 \, 802} + \cdots$
{{OEIS|A006487}}

Proof:
We have by definition of the square root of $2$ that:
:$\sqrt 2 - 1 \approx 0 \cdotp 41421 \, 35623 \, 73095 \, 04880 \ldots$
By inspection:
:$\dfrac 1 3 < \sqrt 2 - 1 < \dfrac 1 2$
Thus:
:$\sqrt 2 - 1 - \dfrac 1 3 \approx 0 \cdotp 08088 \, 02290 \, 39761 \, 71546 \ldots$
Then:
:$\dfrac 1 {13} = 0 \cdotp 07692 \, 3 \ldots$ repeating
and:
:$\dfrac 1 {12} = 0 \cdotp 08333 \ldots$ repeating
and so:
:$\sqrt 2 - 1 - \dfrac 1 3 - \dfrac 1 {13} \approx 0 \cdotp 00395 \, 71521 \, 16684 \, 79239 \cdots$
Thus one can generate this sequence of denominators $\sequence {D_n}$ by:
:$\ds D_n = \ceiling {\paren {\sqrt 2 - \sum_{i \mathop = 0}^{n - 1} \frac 1 {D_i}}^{-1}}$
{{qed}}
Theorem: Sprague's Property of Root 2

Let $S = \sequence {s_n}$ be the sequence of fractions defined as follows:
Let the numerator of $s_n$ be:
:$\floor {n \sqrt 2}$
where $\floor x$ denotes the floor of $x$.
Let the denominators of the terms of $S$ be the (strictly) positive integers missing from the numerators of $S$:
:$S := \dfrac 1 3, \dfrac 2 6, \dfrac 4 {10}, \dfrac 5 {13}, \dfrac 7 {17}, \dfrac 8 {20}, \ldots$
Then the difference between the numerator and denominator of $s_n$ is equal to $2 n$.

Proof:
Denote the numerators of the terms of $S$ as $\sequence {N_n}$.
Denote the denominators of the terms of $S$ as $\sequence {D_n}$.
From the definition:
:$\sequence {N_n}$ is a Beatty sequence, where $\sequence {N_n} = \BB_{\sqrt 2} = \sequence{\floor{n \sqrt 2} }_{n \mathop \in \Z_{> 0} }$
:$\sequence {N_n}$ and $\sequence {D_n}$ are complementary Beatty sequences.
Then by Beatty's Theorem, $\sequence {D_n}$ is a Beatty sequence.
Define $\sequence {D_n} = \BB_y = \sequence{\floor{n y} }_{n \mathop \in \Z_{> 0} }$.
Then we have: 
{{begin-eqn}}
{{eqn | l = \dfrac 1 {\sqrt 2} + \dfrac 1 y
      | r = 1
      | c = Beatty's Theorem
}}
{{eqn | ll = \leadsto
      | l = \dfrac 1 y
      | r = 1 - \dfrac 1 {\sqrt 2}
}}
{{eqn | r = \dfrac {\sqrt 2 - 1} {\sqrt 2}
}}
{{eqn | ll = \leadsto
      | l = y
      | r = \dfrac {\sqrt 2} {\sqrt 2 - 1} 
}}
{{eqn | r = \dfrac {\sqrt 2 \paren {\sqrt 2 + 1} } {\paren {\sqrt 2 - 1} \paren {\sqrt 2 + 1} }
}}
{{eqn | r = 2 + \sqrt 2
}}
{{end-eqn}}
So we have $s_n = \dfrac {N_n} {D_n} = \dfrac {\floor {n \sqrt 2} } {\floor {n \paren {2 + \sqrt 2} } }$.
The difference between the numerator and denominator of $s_n$ is $\floor {n \paren {2 + \sqrt 2} } - \floor {n \sqrt 2}$.
We have:
{{begin-eqn}}
{{eqn | l = \floor {n \paren {2 + \sqrt 2} } - \floor {n \sqrt 2}
      | r = \floor {2 n + n \sqrt 2} - \floor {n \sqrt 2}
}}
{{eqn | r = 2 n + \floor {n \sqrt 2} - \floor {n \sqrt 2}
      | c = Floor of Number plus Integer
}}
{{eqn | r = 2 n
}}
{{end-eqn}}
Hence the result.
{{qed}}
{{Namedfor|Roland Percival Sprague|cat = Sprague, Roland}}
Theorem: Steiner's Calculus Problem

Let $f: \R_{>0} \to \R$ be the real function defined as:
:$\forall x \in \R_{>0}: \map f x = x^{1/x}$
Then $\map f x$ reaches its maximum at $x = e$ where $e$ is Euler's number.

Proof:
{{begin-eqn}}
{{eqn | l = \map {f'} x
      | r = \frac \d {\d x} x^{1/x}
}}
{{eqn | r = \frac \d {\d x} e^{\ln x / x}
}}
{{eqn | r = e^{\ln x / x} \paren {\frac 1 {x^2} - \frac {\ln x} {x^2} }
}}
{{eqn | r = \frac {x^{1/x} } {x^2} \paren {1 - \ln x}
}}
{{end-eqn}}
$\dfrac {x^{1/x} } {x^2}$ is always greater than $0$.
Therefore:
:$\map {f'} x > 0$ for $\ln x < 1$
:$\map {f'} x = 0$ for $\ln x = 1$
:$\map {f'} x < 0$ for $\ln x > 1$
By the Interior Extremum Theorem, the maximum is obtained when $\ln x = 1$.
That is, when $x = e$.
{{qed}}
{{Namedfor|Jakob Steiner|cat = Steiner}}
Theorem: Ratio of Lengths of Arms of Pentagram

Consider a pentagram.
:400px
Let $AC$ be the length of one of the lines which span the pentagram and define it.
Let $B$ be one of the points where $AC$ intersects one of the other such lines such that $AB > AC$.
Then:
:$\dfrac {AC} {AB} = \phi$
where $\phi$ denotes the golden mean.

Proof:
Follows directly from Straight Lines Subtending Two Consecutive Angles in Regular Pentagon cut in Extreme and Mean Ratio.
{{qed}}
{{ProofWanted|Flesh this out}}
Theorem: Filter is Ideal in Dual Ordered Set

Let $P = \struct {S, \preceq}$ be an ordered set.
Let $X$ be a subset of $S$.
Then
:$X$ is filter in $P$
{{iff}}
:$X$ is ideal in $P^{-1}$
where $P^{-1} = \struct {S, \succeq}$ denotes the dual of $P$.

Proof:
By Dual of Dual Ordering:
:dual of $P^{-1}$ is $P$.
Hence by Ideal is Filter in Dual Ordered Set:
:the result follows.
{{qed}}
Theorem: Prime Filter is Prime Ideal in Dual Ordered Set

Let $P = \struct {S, \preceq}$ be a lattice.
Let $X$ be a subset of $S$.
Then
:$X$ is a prime filter of $P$
{{iff}}:
:$X$ is a prime ideal of $P^{-1}$
where $P^{-1} = \struct {S, \succeq}$ denotes the dual of $P$.

Proof:
By Dual of Dual Ordering:
:dual of $P^{-1}$ is $P$.
Hence by Prime Ideal is Prime Filter in Dual Ordered Set:
:the result follows.
{{qed}}
Theorem: Continued Fraction Expansion of Golden Mean/Rate of Convergence

This continued fraction expansion has the slowest rate of convergence of all simple infinite continued fractions.

Proof:
{{ProofWanted|"Rate of convergence" of a CFE needs to be formally defined}}
Theorem: Continued Fraction Expansion of Golden Mean/Successive Convergents

The $n$th convergent is given by:
:$C_n = \dfrac {F_{n + 1} } {F_n}$
where $F_n$ denotes the $n$th Fibonacci number.

Proof:
The proof proceeds by induction.
Listing the first few convergents, which can be calculated:
:$C_1 = \dfrac 1 1$
:$C_2 = \dfrac 2 1$
:$C_3 = \dfrac 3 2$
:$C_4 = \dfrac 5 3$
and so on.
For all $n \in \Z_{> 0}$, let $\map P n$ be the proposition:
:$C_n = \dfrac {F_{n + 1} } {F_n}$
$\map P 1$ is the case:
:$C_1 = \dfrac {F_{n + 1} } {F_n}$
{{begin-eqn}}
{{eqn | l = C_1
      | r = \dfrac 1 1
      | c = 
}}
{{eqn | r = \dfrac {F_2} {F_1}
      | c = {{Defof|Fibonacci Numbers}}
}}
{{end-eqn}}
Thus $\map P 1$ is seen to hold.
Theorem: Continued Fraction Expansion of Pi/Convergents

The convergents of the continued fraction expansion to $\pi$ (pi) are:
:$3, \dfrac {22} 7, \dfrac {333} {106}, \dfrac {355} {113}, \dfrac {103993} {33102}, \dfrac {104348} {33215}$
{{OEIS-Numerators|A002485}}
{{OEIS-Denominators|A002486}}
These best rational approximations are accurate to $0, 2, 4, 6, 9, 9, 9, 10, 11, 11, 12, 13, \ldots$ decimals.
{{OEIS|A114526}}
=== Zu Chongzhi Fraction ===
{{:Definition:Zu Chongzhi Fraction}}

Proof:
{{ProofWanted|Calculation needed}}
Theorem: Filter is Prime iff For Every Element Element either Negation Belongs to Filter in Boolean Lattice

Let $B = \struct {S, \vee, \wedge, \neg, \preceq}$ be a Boolean lattice.
Let $F$ be a filter in $B$.
Then
:$F$ is prime
{{iff}}
:$\forall x \in S: x \in F \lor \paren {\neg x} \in F$

Proof:
=== Sufficient Condition ===
Let $F$ be prime.
Let $x \in S$.
By definition of Boolean lattice:
:$x \vee \neg x = \top$
where $\top$ denotes the top of $B$.
By definition of non-empty set:
:$\exists y: y \in F$
By definition of greatest element:
:$y \preceq \top$
By definition of upper section:
:$\top \in F$
Thus by definition of prime filter:
:$x \in F$ or $\neg x \in F$
{{qed|lemma}}
Theorem: Beatty's Theorem

Let $r, s \in \R \setminus \Q$ be an irrational number such that $r > 1$ and $s > 1$.
Let $\BB_r$ and $\BB_s$ be the Beatty sequences on $r$ and $s$ respectively.
Then $\BB_r$ and $\BB_s$ are complementary Beatty sequences {{iff}}:
:$\dfrac 1 r + \dfrac 1 s = 1$

Proof:
We have been given that $r > 1$.
Let $\dfrac 1 r + \dfrac 1 s = 1$.
Then:
:$s = \dfrac r {r - 1}$
It is to be shown that every positive integer lies in exactly one of the two Beatty sequences $\BB_r$ and $\BB_s$.
Consider the ordinal positions occupied by all the fractions $\dfrac j r$ and $\dfrac k s$ when they are jointly listed in nondecreasing order for positive integers $j$ and $k$.
{{AimForCont}} that $\dfrac j r = \dfrac k s$ for some $j, k \in \Z_{>0}$.
Then:
:$\dfrac r s = \dfrac j k$
which is rational.
But also:
:$\dfrac r s = r \paren {1 - \dfrac 1 r} = r - 1$
which is not rational.
Therefore, no two of the numbers occupy the same position.
Consider some $\dfrac j r$.
There are $j$ numbers $\dfrac i r \le \dfrac j r$.
There are also $\floor {\dfrac {j s} r}$ numbers $\dfrac k s \le \dfrac j r$.
So the position of $\dfrac j r$ in the list is $j + \floor {\dfrac {j s} r}$.
The equation $\dfrac 1 r + \dfrac 1 s = 1$ implies:
:$j + \floor {\dfrac {j s} r} = j + \floor {j \paren {s - 1} } = \floor {j s}$
Likewise, the position of $\dfrac k s$ in the list is $\floor {k r}$.
It is concluded that every positive integer corresponding to every position in the list is of the form $\floor {n r}$ or of the form $\floor {n r}$, but not both.
The converse statement is also true: if $p$ and $q$ are two real numbers such that every positive integer occurs precisely once in the above list, then $p$ and $q$ are irrational and the sum of their reciprocals is $1$.
{{qed}}
Theorem: Beatty's Theorem

Let $r, s \in \R \setminus \Q$ be an irrational number such that $r > 1$ and $s > 1$.
Let $\BB_r$ and $\BB_s$ be the Beatty sequences on $r$ and $s$ respectively.
Then $\BB_r$ and $\BB_s$ are complementary Beatty sequences {{iff}}:
:$\dfrac 1 r + \dfrac 1 s = 1$

Proof:
=== Collisions ===
{{AimForCont}} there exist integers $j > 0, k, m$ such that:
:$j = \floor {k \cdot r} = \floor {m \cdot s}$
This is equivalent to the inequalities:
:$j \le k \cdot r < j + 1$
and:
:$j \le m \cdot s < j + 1$
As $r$ and $s$ are irrational, equality cannot happen.
So:
:$j < k \cdot r < j + 1$
and:
:$j < m \cdot s < j + 1$
which leads to:
:$\dfrac j r < k < \dfrac {j + 1} r$
and:
:$\dfrac j s < m < \dfrac {j + 1} s$
Adding these together and using the by hypothesis:
:$j < k + m < j + 1$
Thus there is an integer strictly between two adjacent integers.
This is impossible.
Thus the supposition must be false.
{{qed|lemma}}
=== Anti-collisions ===
{{AimForCont}} that there exist integers $j > 0, k, m$ such that:
:$k \cdot r < j$
and:
:$j + 1 \le \paren {k + 1} \cdot r$
and:
:$m \cdot s < j$
and:
:$j + 1 \le \paren {m + 1} \cdot s$
Since $j + 1 \ne 0$, and $r$ and $s$ are irrational, equality cannot happen.
So:
:$k \cdot r < j$
and:
:$j + 1 < \paren {k + 1} \cdot r$
and:
:$m \cdot s < j$
and:
:$j + 1 < \paren {m + 1} \cdot s$
Then:
:$k < \dfrac j r$:
and:
:$\dfrac {j + 1} r < k + 1$
and:
:$m < \dfrac j s$
and:
:$\dfrac {j + 1} s < m + 1$
Adding corresponding inequalities:
:$k + m < j$
and:
:$j + 1 < k + m + 2$
:$k + m < j < k + m + 1$
which is also impossible.
Thus the supposition is false.
{{qed}}
Theorem: Proper and Prime iff Ultrafilter in Boolean Lattice

Let $B = \struct {S, \vee, \wedge, \neg, \preceq}$ be a Boolean lattice.
Let $F$ be a filter in $B$.
Then
:$F$ is a proper subset of $S$ and $F$ is a prime filter in $B$
{{iff}}:
:$F$ is ultrafilter on $B$

Proof:
=== Sufficient Condition ===
Let us assume
:$F$ is a proper subset of $S$ and $F$ is a prime filter in $B$.
Thus
:$F$ is a proper subset of $S$.
Let $G$ be a filter in $B$ such that
:$F \subseteq G$ and $F \ne G$.
By definitions of subset and set equality:
:$\exists x: x \in G \land x \notin F$
By definition of Boolean algebra:
:$x \vee \neg x = \top$
where $\top$ denotes the top of $B$.
By Top in Filter:
:$\top \in F$
By definition of prime filter:
:$\neg x \in F$
By definition of subset:
:$\neg x \in G$
By Filtered in Meet Semilattice:
:$x \wedge \neg x \in G$
By definition of Boolean algebra:
:$\bot \in G$
Thus by definition of subset:
:$G \subseteq S$
By definition of set equality it remains to prove that
:$S \subseteq G$
Let $y \in S$.
By definition of smallest element:
:$\bot \preceq y$
Thus by definition of upper section:
:$y \in G$
{{qed|lemma}}
Theorem: Equivalence of Definitions of Upper Wythoff Sequence

The following definitions of the upper Wythoff sequence are equivalent:

Proof:
From Beatty's Theorem, the Beatty sequences $\BB_r$ and $\BB_s$ are complementary {{iff}}:
:$\dfrac 1 r + \dfrac 1 s = 1$
It remains to be demonstrated that this holds for $r = \phi$ and $s = \phi^2$.
Thus:
{{begin-eqn}}
{{eqn | l = \dfrac 1 \phi + \dfrac 1 {\phi^2}
      | r = \dfrac {\phi + 1} {\phi^2}
      | c = 
}}
{{eqn | r = \dfrac {\phi^2} {\phi^2}
      | c = Square of Golden Mean equals One plus Golden Mean
}}
{{eqn | r = 1
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Category:Beatty Sequences
3nsf04gdm0byuleucl1pa4oql7ec93n
Theorem: Difference between Terms of Wythoff Pair

Let $\tuple {\floor {k \phi}, \floor {k \phi^2} }$ be a Wythoff pair.
The difference between the coordinates of this Wythoff pair is $k$.
That is:
:$\floor {k \phi^2} - \floor {k \phi} = k$

Proof:
{{begin-eqn}}
{{eqn | l = \floor {k \phi^2}
      | r = \floor {k \paren {1 + \phi} }
      | c = Square of Golden Mean equals One plus Golden Mean
}}
{{eqn | r = \floor {k + k \phi}
      | c = 
}}
{{eqn | r = k + \floor {k \phi}
      | c = 
}}
{{end-eqn}}
{{qed}}