avewright/proofwiki-math huggingface dataset:
Theorem: Solutions of Diophantine Equation x^4 + y^4 = z^2 + 1 for x = 239

Consider the indeterminate Diophantine equation:
:$x^4 + y^4 = z^2 + 1$
When $x = 239$ and $x > y$, there are $3$ solutions:
{{begin-eqn}}
{{eqn | l = 239^4 + 104^4
      | r = 58 \, 136^2 + 1
      | c = 
}}
{{eqn | l = 239^4 + 143^4
      | r = 60 \, 671^2 + 1
      | c = 
}}
{{eqn | l = 239^4 + 208^4
      | r = 71 \, 656^2 + 1
      | c = 
}}
{{end-eqn}}

Proof:
{{ProofWanted|It remains to be shown there are no other solutions. This can be achieved by brute force. For this page, it is then adequate to present a pseudocode program to illustrate it.}}
Theorem: Smallest Numbers with 240 Divisors

The smallest integers with $240$ divisors are:
:$720 \, 720, 831 \, 600, 942 \, 480, 982 \, 800, 997 \, 920, \ldots$

Proof:
In the below, $\map {\sigma_0} n$ denotes the divisor count function of $n$.
Then:
{{begin-eqn}}
{{eqn | l = \map {\sigma_0} {720 \, 720}
      | r = 240
      | c = {{DCFLink|720,720|720 \, 720}}
}}
{{eqn | l = \map {\sigma_0} {831 \, 600}
      | r = 240
      | c = {{DCFLink|831,600|831 \, 600}}
}}
{{eqn | l = \map {\sigma_0} {942 \, 480}
      | r = 240
      | c = {{DCFLink|942,480|942 \, 480}}
}}
{{eqn | l = \map {\sigma_0} {982 \, 800}
      | r = 240
      | c = {{DCFLink|982,800|982 \, 800}}
}}
{{eqn | l = \map {\sigma_0} {997 \, 920}
      | r = 240
      | c = {{DCFLink|997,920|997 \, 920}}
}}
{{end-eqn}}
{{ProofWanted|Prove that these are indeed the smallest}}
Theorem: Sequence of 4 Consecutive Integers with Equal Number of Divisors

The following sequence of integers are sets of $4$ consecutive integers which all have the same number of divisors:
:$\map {\sigma_0} m = \map {\sigma_0} {m + 1} = \map {\sigma_0} {m + 2} = \map {\sigma_0} {m + 3}$
where $\map {\sigma_0} n$ denotes the divisor count function.
:$242, 243, 244, 245, 3655, 3656, 3657, 3658, 4503, 4504, 4505, 4506, \ldots$
{{OEIS|A039665}}

Proof:
{{begin-eqn}}
{{eqn | l = \map {\sigma_0} {242}
      | r = 6
      | c = {{DCFLink|242}}
}}
{{eqn | l = \map {\sigma_0} {243}
      | r = 6
      | c = {{DCFLink|243}}
}}
{{eqn | l = \map {\sigma_0} {244}
      | r = 6
      | c = {{DCFLink|244}}
}}
{{eqn | l = \map {\sigma_0} {245}
      | r = 6
      | c = {{DCFLink|245}}
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \map {\sigma_0} {3655}
      | r = 8
      | c = {{DCFLink|3655}}
}}
{{eqn | l = \map {\sigma_0} {3656}
      | r = 8
      | c = {{DCFLink|3656}}
}}
{{eqn | l = \map {\sigma_0} {3657}
      | r = 8
      | c = {{DCFLink|3657}}
}}
{{eqn | l = \map {\sigma_0} {3658}
      | r = 8
      | c = {{DCFLink|3658}}
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of 2 Squares in 2 Distinct Ways which is also Sum of Cubes/Sequence

The  sequence of positive integers which are both the sum of $2$ square numbers in two distinct ways and also the sum of $2$ cube numbers begins:
:$65, 250, \ldots$

Proof:
{{begin-eqn}}
{{eqn | l = 65
      | r = 4^3 + 1^3
      | c = 
}}
{{eqn | r = 8^2 + 1^2
      | c = 
}}
{{eqn | r = 7^2 + 4^2
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = 250
      | r = 5^3 + 5^3
      | c = 
}}
{{eqn | r = 15^2 + 5^2
      | c = 
}}
{{eqn | r = 13^2 + 9^2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Equivalence of Definitions of Balanced Prime

The following definitions of a balanced prime are equivalent:

Proof:
{{begin-eqn}}
{{eqn | l = p_n
      | r = \dfrac {p_{n - 1} + p_{n + 1} } 2
      | c = {{Defof|Balanced Prime|index = 1}}
}}
{{eqn | ll= \leadstoandfrom
      | l = 2 p_n
      | r = p_{n - 1} + p_{n + 1}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = p_n - p_{n - 1}
      | r = p_{n + 1} - p_n
      | c = {{Defof|Balanced Prime|index = 3}}: equal prime gaps
}}
{{eqn | r = d
      | c = for some $d \in \Z$
}}
{{eqn | ll= \leadstoandfrom
      | l = p_{n - 1} + d
      | r = p_n
      | c = {{Defof|Balanced Prime|index = 2}}
}}
{{eqn | l = p_{n - 1} + 2 d
      | r = p_{n + 1}
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Balanced Primes
kzripv762lbfjbspoh6hq0xwm258rmp
Theorem: Filtered iff Directed in Dual Ordered Set

Let $\struct {S, \preceq_1}$ be an ordered set.
Let $\struct {S, \preceq_2}$ be a dual ordered set of $\struct {S, \preceq_1}$
Let $X \subseteq S$.
Then:
:$X$ is filtered in $\struct {S, \preceq_1}$
{{iff}}:
:$X$ is directed in $\struct {S, \preceq_2}$

Proof:
By Dual of Dual Ordering:
:$\struct {S, \preceq_1}$ is the dual of $\struct {S, \preceq_2}$.
Thus by Directed iff Filtered in Dual Ordered Set:
:$X$ is filtered in $\struct {S, \preceq_1}$
{{iff}}:
:$X$ is directed in $\struct {S, \preceq_2}$.
{{qed}}
Theorem: Filters equal Ideals in Dual Ordered Set

Let $L_1 = \struct {S, \preceq_1}$ be an ordered set.
Let $L_2 = \struct {S, \preceq_2}$ be a dual ordered set of $L_1$.
Then $\map {\mathit {Filt} } {L_1} = \map {\mathit {Ids} } {L_2}$
where
:$\map {\mathit {Filt} } {L_1}$ denotes the set of all filters of $L_1$,
:$\map {\mathit {Ids} } {L_2}$ denotes the set of all ideals of $L_2$.

Proof:
Let $x$ be a set.
By definition of $\mathit {Filt}$:
:$x \in \map {\mathit {Filt} } {L_1} \iff x$ is a filter on $L_1$.
By Filter is Ideal in Dual Ordered Set:
:$x \in \map {\mathit {Filt} } {L_1} \iff x$ is an ideal in $L_2$.
By definition of $\mathit{Ids}$:
:$x \in \map {\mathit {Filt} } {L_1} \iff x \in \map {\mathit {Ids} } {L_2}$
Hence by definition of set equality:
:$\map {\mathit {Filt} } {L_1} = \map {\mathit {Ids} } {L_2}$
{{qed}}
Theorem: Pépin's Test

Let $F_n = 2^{2^n} + 1$ be a Fermat number.
Then $F_n$ is prime {{iff}}:
:$3^{\paren {F_n - 1} / 2} \equiv -1 \pmod {F_n}$

Proof:
=== Sufficient Condition ===
Let this congruence hold:
:$3^{\paren {F_n - 1} / 2} \equiv -1 \pmod {F_n}$
Then:
:$3^{F_n - 1} \equiv 1 \pmod {F_n}$
Thus the multiplicative order of $3$ modulo $F_n$ is a divisor of $F_n - 1 = 2^{2^n}$.
This is a power of $2$.
On the other hand, the multiplicative order of $3$ modulo $F_n$ is not a divisor of $\dfrac {F_n - 1} 2$.
Therefore it must be equal to $F_n - 1$.
In particular, there are at least $F_n - 1$ numbers below $F_n$ which are coprime to $F_n$.
This can happen only if $F_n$ is prime.
{{qed|lemma}}
Theorem: Triangular Fermat Number

The only one Fermat number which is triangular is $3$.

Proof:
Let $F_n$ be a Fermat number which is triangular.
We use the weaker form of Divisor of Fermat Number:
:Every divisor of $F_n$ is of the form $k \times 2^{n + 1} + 1$
as this formulation is valid for all $n \in \N$.
From Closed Form for Triangular Numbers:
:$F_n = \dfrac {m \paren {m + 1} } 2$
Either $m$ or $m + 1$ is even.
Suppose $m$ is even.
Then:
{{begin-eqn}}
{{eqn | q = \exists k \in \N
      | l = \frac m 2
      | r = k \times 2^{n + 1} + 1
      | c = Divisor of Fermat Number
}}
{{eqn | ll= \leadsto 
      | l = m + 1
      | r = 2 \paren {k \times 2^{n + 1} + 1} + 1
}}
{{eqn | r = k \times 2^{n + 2} + 3
}}
{{eqn | q = \exists j \in \N
      | l = m + 1
      | r = j \times 2^{n + 1} + 1
      | c = Divisor of Fermat Number
}}
{{eqn | ll= \leadsto
      | l = k \times 2^{n + 2} + 2
      | r = j \times 2^{n + 1}
}}
{{eqn | ll= \leadsto
      | l = k \times 2^{n + 1} + 1
      | r = j \times 2^n
}}
{{end-eqn}}
As the {{LHS}} is always odd, we must have $2^n = 1$.
This forces $n = 0$, with $F_n = 3$.
We check that $3$ is indeed a triangular number.
Suppose $m + 1$ is even.
Then:
{{begin-eqn}}
{{eqn | q = \exists k \in \N
      | l = \frac {m + 1} 2
      | r = k \times 2^{n + 1} + 1
      | c = Divisor of Fermat Number
}}
{{eqn | ll= \leadsto 
      | l = m
      | r = 2 \paren {k \times 2^{n + 1} + 1} - 1
}}
{{eqn | r = k \times 2^{n + 2} + 1
}}
{{eqn | l = F_n
      | r = \frac {m \paren {m + 1} } 2
}}
{{eqn | ll= \leadsto
      | l = 2^{2^n} + 1
      | r = \paren {k \times 2^{n + 2} + 1} \paren {k \times 2^{n + 1} + 1}
}}
{{eqn | r = k^2 \times 2^{2 n + 3} + k \paren {2^{n + 2} + 2^{n + 1} } + 1
}}
{{eqn | ll= \leadsto
      | l = 2^{2^n}
      | r = k^2 \times 2^{2 n + 3} + k \paren {2^{n + 2} + 2^{n + 1} }
}}
{{eqn | r = k \times 2^{n + 1} \times \paren {k \times 2^{n + 2} + 3 }
}}
{{end-eqn}}
As $k \times 2^{n + 2} + 3 > 1$ and is odd, $k \times 2^{n + 2} + 3$ cannot be a power of $2$.
So $m + 1$ cannot be even, and we have exhausted all possibilities.
{{qed}}
Theorem: Fermat Number is not Square

There exist no Fermat numbers which are square.

Proof:
Recall the definition of Fermat numbers:
:$F_n = 2^{(2^n)}+1$, where $n = 0, 1, 2, \ldots$
=== Marginal Case ===
$F_0 = 3$ is not a square.
=== General Case ===
It will be shown that Fermat numbers lie between $2$ consecutive squares, thus cannot be itself a square:
{{begin-eqn}}
{{eqn | l = \left({2^{ \left({2^{n-1} }\right)} }\right)^2
      | r = 2^{\left({2^n}\right)}
      | c = Index Laws/Product of Indices
}}
{{eqn | o = <
      | r = 2^{\left({2^n}\right)} + 1
      | c = adding a positive term
}}
{{eqn | r = F_n
      | c = 
}}
{{eqn | o = <
      | r = 2^{\left({2^n}\right)} + 2^{\left({2^{n-1} }\right) + 1} + 1
      | c = adding another positive term
}}
{{eqn | r = \left({2^{\left({2^{n-1} }\right)} + 1}\right)^2
      | c = Completing the Square
}}
{{end-eqn}}
{{qed}}
Theorem: Fermat Number is not Cube

There exist no Fermat numbers which are cubes.

Proof:
Direct consequence of Fermat Number is not Perfect Power.
{{qed}}
Theorem: Construction of Regular 257-Gon

It is possible to construct a regular polygon with $257$ sides using a compass and straightedge construction.

Proof:
257 is a Fermat prime.
From Construction of Regular Prime $p$-Gon Exists iff $p$ is Fermat Prime it is known that this construction is possible.
{{qed}}
Theorem: Ideals equal Filters in Dual Ordered Set

Let $L_1 = \struct {S, \preceq_1}$ be an ordered set.
Let $L_2 = \struct {S, \preceq_2}$ be a dual ordered set of $L_1$.
Then $\map {\mathit {Ids} } {L_1} = \map {\mathit {Filt} } {L_2}$
where
:$\map {\mathit {Filt} } {L_2}$ denotes the set of all filters of $L_2$
:$\map {\mathit {Ids} } {L_1}$ denotes the set of all ideals of $L_1$.

Proof:
Let $x$ be a set.
By definition of $\mathit {Filt}$:
:$x \in \map {\mathit {Filt} } {L_2} \iff x$ is a filter on $L_2$.
By Ideal is Filter in Dual Ordered Set:
:$x \in \map {\mathit {Filt} } {L_2} \iff x$ is an ideal in $L_1$.
By definition of $\mathit{Ids}$:
:$x \in \map {\mathit {Filt} } {L_2} \iff x \in \map {\mathit {Ids} } {L_1}$
Hence by definition of set equality:
:$\map {\mathit {Ids} } {L_1} = \map {\mathit {Filt} } {L_2}$
{{qed}}
Theorem: Power Set is Filter in Lattice of Power Set

Let $X$ be a set.
Let $L = \struct {\powerset X, \cup, \cap, \subseteq}$ be a inclusion lattice of power set of $X$.
Then $\powerset X$ is a filter on $L$.

Proof:
=== Filtered ===
By Set is Element of its Power Set:
:$X \in \powerset X$
Thus by definition:
:$\powerset X$ is a non-empty set.
Let $x, y \in \powerset X$.
By Intersection is Subset:
:$x \cap y \subseteq x$ and $x \cap y \subseteq y$
By Subset Relation is Transitive:
:$x \cap y \in \powerset X$
Thus
:$\exists z \in \powerset X: z \subseteq x \land z \subseteq y$
{{qed|lemma}}
Theorem: Triplet in Arithmetic Sequence with equal Divisor Sum

The smallest triple of integers in arithmetic sequence which have the same divisor sum is:
:$\map {\sigma_1} {267} = \map {\sigma_1} {295} = \map {\sigma_1} {323} = 360$

Proof:
We have that:
{{begin-eqn}}
{{eqn | l = 295 - 267
      | r = 28
      | c = 
}}
{{eqn | l = 323 - 295
      | r = 28
      | c = 
}}
{{end-eqn}}
demonstrating that $267, 295, 323$ are in arithmetic sequence with common difference $28$.
Then:
{{begin-eqn}}
{{eqn | l = \map {\sigma_1} {267}
      | r = 360
      | c = {{DSFLink|267}}
}}
{{eqn | l = \map {\sigma_1} {295}
      | r = 360
      | c = {{DSFLink|295}}
}}
{{eqn | l = \map {\sigma_1} {323}
      | r = 360
      | c = {{DSFLink|323}}
}}
{{end-eqn}}
{{ProofWanted|It remains to be shown that these are the smallest.}}
Theorem: Singleton of Set is Filter in Lattice of Power Set

Let $X$ be a set.
Let $L = \struct {\powerset X, \cup, \cap, \subseteq}$ be an inclusion lattice of power set of $X$.
Then $\set X$ is a filter on $L$.

Proof:
By Singleton is Directed and Filtered Subset:
:$\set X$ is filtered.
We will prove that
:$\set X$ is an upper section.
Let $x \in \set X$, $y \in \powerset X$ such that:
:$x \subseteq y$
By definition of singleton:
:$x = X$
By definition of power set:
:$y \subseteq X$
By definition of set equality:
:$y = X$
Thus:
:$y \in \set X$
{{qed|lemma}}
Thus by definition of filter in ordered set:
:$\set X$ is a filter.
{{qed}}
Theorem: Consecutive Triple of Repeated Digit-Products

The triplet of integers $281, 282, 283$ have the property that if their digits are multiplied, and the process repeated on the result until only $1$ digit remains, that final digit is the same for all three, that is, $6$.
There does not exist an set of four consecutive integers which also all end up at the same single digit.

Proof:
{{begin-eqn}}
{{eqn | ll= 281:
      | l = 2 \times 8 \times 1
      | r = 16
      | c = 
}}
{{eqn | l = 1 \times 6
      | r = 6
      | c = 
}}
{{eqn | ll= 282:
      | l = 2 \times 8 \times 2
      | r = 32
      | c = 
}}
{{eqn | l = 3 \times 2
      | r = 6
      | c = 
}}
{{eqn | ll= 283:
      | l = 2 \times 8 \times 3
      | r = 48
      | c = 
}}
{{eqn | l = 4 \times 8
      | r = 32
      | c = 
}}
{{eqn | l = 3 \times 2
      | r = 6
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Consecutive Powerful Numbers

The following pairs are of consecutive positive integers both of which are powerful:
:$\left({8, 9}\right), \left({288, 289}\right), \left({675, 676}\right), \left({9800, 9801}\right), \left({332 \, 928, 332 \, 929}\right), \ldots$
{{OEIS|A060355}}

Proof:
{{begin-eqn}}
{{eqn | l = 8
      | r = 2^3
}}
{{eqn | l = 9
      | r = 3^2
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = 288
      | r = 2^5 \times 3^2
}}
{{eqn | l = 289
      | r = 17^2
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = 675
      | r = 3^3 \times 5^2
}}
{{eqn | l = 676
      | r = 2^2 \times 13^2
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = 9800
      | r = 2^3 \times 5^2 \times 7^2
}}
{{eqn | l = 9801
      | r = 3^4 \times 11^2
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = 332 \, 928
      | r = 2^7 \times 3^2 \times 17^2
}}
{{eqn | l = 332 \, 929
      | r = 577^2
}}
{{end-eqn}}
{{qed}}
Theorem: Smallest Multiple of 9 with all Digits Even

$288$ is the smallest integer multiple of $9$ all of whose digits are even.

Proof:
By the brute force technique:
{{begin-eqn}}
{{eqn | l = 1 \times 9
      | r = 9
}}
{{eqn | l = 2 \times 9
      | r = 18
}}
{{eqn | l = 3 \times 9
      | r = 27
}}
{{eqn | l = 4 \times 9
      | r = 36
}}
{{eqn | l = 5 \times 9
      | r = 45
}}
{{eqn | l = 6 \times 9
      | r = 54
}}
{{eqn | l = 7 \times 9
      | r = 63
}}
{{eqn | l = 8 \times 9
      | r = 72
}}
{{eqn | l = 9 \times 9
      | r = 81
}}
{{eqn | l = 10 \times 9
      | r = 90
}}
{{eqn | l = 11 \times 9
      | r = 99
}}
{{eqn | l = 12 \times 9
      | r = 108
}}
{{end-eqn}}
All integer multiples of $9$ $k \times 9$ for $k = 12$ through to $k = 22$ begin with $1$, and so have at least one odd digit.
Then:
{{begin-eqn}}
{{eqn | l = 22 \times 9
      | r = 198
}}
{{eqn | l = 23 \times 9
      | r = 207
}}
{{eqn | l = 24 \times 9
      | r = 216
}}
{{eqn | l = 25 \times 9
      | r = 225
}}
{{eqn | l = 26 \times 9
      | r = 234
}}
{{eqn | l = 27 \times 9
      | r = 243
}}
{{eqn | l = 28 \times 9
      | r = 252
}}
{{eqn | l = 39 \times 9
      | r = 261
}}
{{eqn | l = 30 \times 9
      | r = 270
}}
{{eqn | l = 31 \times 9
      | r = 279
}}
{{eqn | l = 32 \times 9
      | r = 288
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Smallest Multiple of 9 with all Digits Even

$288$ is the smallest integer multiple of $9$ all of whose digits are even.

Proof:
Let $n$ be the smallest integer multiple of $9$ all of whose digits are even.
From Divisibility by 9, the digits of $n$ must add to an integer multiple of $9$.
But from Sum of Even Integers is Even, the digits of $n$ must add to an even integer multiple of $9$: $18, 36, 54$, etc.
There is only $1$ integer multiple of $9$ with $2$ digits whose digits add to an even integer multiple of $9$, and that is $99$.
Thus we have to look at $3$-digit integers.
The following sets of $3$ even digits add to $18$:
:$\set {2, 8, 8}$
:$\set {4, 6, 8}$
:$\set {6, 6, 6}$
and that seems to be about it.
There are no sets of $3$ even digits which add up to $36$ or higher.
The result follows by inspection.
{{qed}}
Theorem: Kaprekar's Symmetry

Let $n$ be a Kaprekar number with $D$ digits.
Then $10^D - n$ is also a Kaprekar number.

Proof:
Since $n$ is a Kaprekar number of $D$ digits:
:$\begin {cases} n^2 = a \times 10^D + b \\ n = a + b \end {cases}$
for some positive integers $a$ and $b$, $b < 10^D$.
Hence:
{{begin-eqn}}
{{eqn | l = \paren {10^D - n}^2
      | r = 10^{2 D} - 2 n \times 10^D + n^2
}}
{{eqn | r = 10^{2 D} - 2 \paren {a + b} 10^D + a \times 10^D + b
}}
{{eqn | r = 10^D \paren {10^D - a - 2 b} + b
}}
{{end-eqn}}
and we have:
:$\paren {10^D - a - 2 b} + b = 10^D - a - b = 10^D - n$
Finally we check that $10^D - a - 2 b \ge 0$:
{{AimForCont}} $10^D - a - 2 b \le -1$.
Then:
{{begin-eqn}}
{{eqn | l = \paren {10^D - n}^2
      | r = 10^D \paren {10^D - a - 2 b} + b
}}
{{eqn | o = \le
      | r = -10^D + b
}}
{{eqn | o = <
      | r = 0
}}
{{end-eqn}}
but squares are positive, a contradiction.
Hence $10^D - n$ is also a Kaprekar number of $D$ digits.
{{qed}}
{{Namedfor|Dattathreya Ramchandra Kaprekar|cat = Kaprekar}}
Theorem: Difference between Kaprekar Number and Square is Multiple of Repunit

Let $n$ be a Kaprekar number of $m$ digits.
Then:
: $n^2 - n = k R_m$
where:
:$R_m$ is the $m$-digit repunit
:$k$ is an integer.

Proof:
Since $n$ is a Kaprekar number of $m$ digits:
:$\begin {cases} n^2 = a \times 10^m + b \\ n = a + b \end {cases}$
for some positive integers $a$ and $b$.
Hence:
{{begin-eqn}}
{{eqn | l = n^2 - n
      | r = a \times 10^m + b - a - b
}}
{{eqn | r = a \paren {10^m - 1}
}}
{{eqn | r = 9 a R_m
}}
{{end-eqn}}
{{qed}}
Theorem: Filters of Lattice of Power Set form Bounded Above Ordered Set

Let $X$ be a set.
Let $L = \struct {\powerset X, \cup, \cap, \subseteq}$ be an inclusion lattice of power set of $X$.
Let $F = \struct {\map {\operatorname{Filt} } L, \subseteq}$ be an inclusion ordered set,
where $\map {\operatorname{Filt} } L$ denotes the set of all filters on $L$.
Then $F$ is bounded above and $\top_F = \powerset X$
where $\top_F$ denotes the greatest element of $F$.

Proof:
By Power Set is Filter in Lattice of Power Set:
:$\powerset X$ is a filter on $L$.
Let $A \in \map {\operatorname{Filt} } L$.
Thus by definition of filter:
:$A \subseteq \powerset X$
Thus by definitions:
:$F$ is bounded above and $\top_F = \powerset X$
{{qed}}
Theorem: Filters of Lattice of Power Set form Bounded Below Ordered Set

Let $X$ be a set.
Let $L = \struct {\powerset X, \cup, \cap, \subseteq}$ be an inclusion lattice of power set of $X$.
Let $F = \struct {\map {\operatorname {Filt} } L, \subseteq}$ be an inclusion ordered set,
where $\map {\operatorname {Filt} } L$ denotes the set of all filters on $L$.
Then $F$ is bounded below and $\bot_F = \set X$
where $\bot_F$ denotes the smallest element of $F$.

Proof:
By Singleton of Set is Filter in Lattice of Power Set:
:$\set X$ is a filter on $L$.
Let $A \in \map {\operatorname {Filt} } L$.
By definition of non-empty set:
:$\exists x: x \in A$
By definition of power set:
:$x \subseteq X$
By definition of upper section:
:$X \in A$
Thus by definitions of singleton and subset:
:$\set X \subseteq A$
Thus by definitions:
:$F$ is bounded below and $\bot_F = \set X$
{{qed}}
Theorem: Palindromic Primes in Base 10 and Base 2

The following $n \in \Z$ are prime numbers which are palindromic in both decimal and binary:
:$3, 5, 7, 313, 7 \, 284 \, 717 \, 174 \, 827, 390 \, 714 \, 505 \, 091 \, 666 \, 190 \, 505 \, 417 \, 093, \ldots$
{{OEIS|A046472}}
It is not known whether there are any more.

Proof:
:{| border="1"
|-
! align="center" style = "padding: 2px 10px" | $n_{10}$ 
! align="center" style = "padding: 2px 10px" | $n_2$ 
|-
| align="right" style = "padding: 2px 10px" | $3$
| align="right" style = "padding: 2px 10px" | $11$
|-
| align="right" style = "padding: 2px 10px" | $5$
| align="right" style = "padding: 2px 10px" | $101$
|-
| align="right" style = "padding: 2px 10px" | $7$
| align="right" style = "padding: 2px 10px" | $111$
|-
| align="right" style = "padding: 2px 10px" | $313$
| align="right" style = "padding: 2px 10px" | $100 \, 111 \, 001$
|-
| align="right" style = "padding: 2px 10px" | $7 \, 284 \, 717 \, 174 \, 827$
| align="right" style = "padding: 2px 10px" | $1 \, 101 \, 010 \, 000 \, 000 \, 011 \, 010 \, 111 \, 110 \, 101 \, 100 \, 000 \, 000 \, 101 \, 011$
|-
| align="right" style = "padding: 2px 10px" | $390 \, 714 \, 505 \, 091 \, 666 \, 190 \, 505 \, 417 \, 093$
| align="right" style = "padding: 2px 10px" | $10 \, 100 \, 001 \, 100 \, 110 \, 001 \, 000 \, 000 \, 111 \, 100 \, 001 \, 100 \, 011 \, 000 \, 111 \, 011 \, 100 \, 011 \, 000 \, 110 \, 000 \, 111 \, 100 \, 000 \, 010 \, 001 \, 100 \, 110 \, 000 \, 101$
|}
The last two numbers have $43$ and $89$ digits (in binary) respectively .
{{qed}}
Theorem: Ideals form Complete Lattice

Let $L = \struct {S, \vee, \preceq}$ be a bounded below join semilattice.
Let $\II = \struct {\map {\operatorname{Ids} } L, \subseteq}$ be an inclusion ordered set,
where $\map {\operatorname{Ids} } L$ denotes the set of all ideals in $L$.
Then $\II$ is complete lattice.

Proof:
Let $X \subseteq \map {\operatorname{Ids} } L$.
By Intersection of Semilattice Ideals is Ideal/Set of Sets:
:$\ds \bigcap X$ is an ideal.
By Intersection is Largest Subset/General Result:
:$\ds \forall A \in \map {\operatorname{Ids} } L: \paren {\forall I \in X: A \subseteq I} \iff A \subseteq \bigcap X$
Thus by definition:
:$X$ admits an infimum.
Thus by dual to Lattice is Complete iff it Admits All Suprema:
:$\II$ is complete lattice.
{{qed}}
Theorem: Filters form Complete Lattice

Let $L = \left({S, \wedge, \preceq}\right)$ be a bounded above meet semilattice.
Let $F = \left({\mathit{Filt}\left({L}\right), \subseteq}\right)$ be an inclusion ordered set,
where $\mathit{Filt}\left({L}\right)$ denotes set of all filters on $L$.
Then $F$ is a complete lattice.

Proof:
Define $L^{-1} := \left({S, \succeq}\right)$ be a dual ordered set of $L$.
By Dual Pairs (Order Theory):
:$L^{-1}$ is a bounded below meet semilattice.
By Filters equal Ideals in Dual Ordered Set:
:$\mathit{Filt}\left({L}\right) = \mathit{Ids}\left({L^{-1} }\right)$
where $\mathit{Ids}\left({L^{-1} }\right)$ denotes the set of all ideals in $L^{-1}$.
Thus by Ideals form Complete Lattice:
:$F$ is a complete lattice.
{{qed}}
Theorem: 319 is not Expressible as Sum of Fewer than 19 Fourth Powers

:$319 = 15 \times 1^4 + 3 \times 2^4 + 4^4$
or:
:$319 = 12 \times 1^4 + 4 \times 2^4 + 3 \times 3^4$

Proof:
First note that $5^4 = 625 > 319$.
Then note that $2 \times 4^4 = 512 > 319$.
Hence any expression of $319$ as fourth powers uses no $n^4$ for $n \ge 5$, and uses not more than $1$ instance of $4^4$.
For the remainder, using $2^4$ uses fewer fourth powers than $16$ instances of $1^4$.
Now we have:
{{begin-eqn}}
{{eqn | l = 319
      | r = 4^4 + 3 \times 2^4 + 15 \times 1^4
}}
{{eqn | r = 3 \times 3^4 + 4 \times 2^4 + 12 \times 1^4
}}
{{eqn | r = 2 \times 3^4 + 9 \times 2^4 + 13 \times 1^4
}}
{{eqn | r = 1 \times 3^4 + 14 \times 2^4 + 14 \times 1^4
}}
{{eqn | r = 0 \times 3^4 + 19 \times 2^4 + 15 \times 1^4
}}
{{end-eqn}}
and it can be seen that the first two use the least number of fourth powers, at $19$.
{{qed}}
Theorem: Existence of n such that M - 2^n or M + 2^n has no Prime factors less than 331

Let $M \in \Z$ be an integer.
Then there exists a positive integer $n \in \Z_{\ge 0}$ such that either $M - 2^n$ or $M + 2^n$ has no prime factors less than $331$.

Proof:
{{ProofWanted|Arises during the course of Not Every Number is the Sum or Difference of Two Prime Powers and may be either a lemma or corollary -- hence may require a rename.  Work is needed to analyse that result.}}