avewright/proofwiki-math huggingface dataset:
Theorem: Odd Squares 7 Less than Nearest Power of 2

There exist exactly $3$ odd squares which are $7$ less than the nearest power of $2$:
:$5^2 = 25 = 2^5 - 7$
:$11^2 = 121 = 2^7 - 7$
:$181^2 = 32 \, 761 = 2^{15} - 7$
{{OEIS|A038198}}
Note that this sequence includes $1$ and $3$, being all the squares which are $7$ less than a power of $2$.
However, for $1$ and $3$, those powers ($8$ and $16$ respectively) are not the nearest power of $2$ ($1$ and $4$ respectively).

Proof:
From Solutions of Ramanujan-Nagell Equation, the only solutions to the equation:
:$x^2 + 7 = 2^n$
are $\tuple {x, n} =$:
:$\tuple {1, 3}, \tuple {3, 4}, \tuple {5, 5}, \tuple {11, 7}, \tuple {181, 15}$
so no more solutions exist.
{{qed}}
Theorem: Successive Solutions of Phi of n equals Phi of n + 2

$7$ and $8$ are two successive integers which are solutions to the equation:
:$\map \phi n = \map \phi {n + 2}$

Proof:
From Euler Phi Function of Prime:
:$\map \phi 7 = 7 - 1 = 6$
From Euler Phi Function of Prime Power:
:$\map \phi 9 = \map \phi {3^2} = 2 \times 3^{2 - 1} = 6 = \map \phi 7$
From {{Corollary|Euler Phi Function of Prime Power}}:
:$\map \phi 8 = \map \phi {2^3} = 2^{3 - 1} = 4$
From Euler Phi Function of Integer:
:$\map \phi {10} = \map \phi {2 \times 5} = 10 \paren {1 - \dfrac 1 2} \paren {1 - \dfrac 1 5} = 10 \times \dfrac 1 2 \times \dfrac 4 5 = 4 = \map \phi 8$
{{qed}}
Theorem: Sums of Sequences of Consecutive Squares which are Square

The sums of the following sequences of successive squares are themselves square:
{{begin-eqn}}
{{eqn | l = \sum_{i \mathop = 7}^{29} k^2
      | r = 7^2 + 8^2 + \cdots + 29^2
      | c = 
}}
{{eqn | l = \sum_{i \mathop = 7}^{39} k^2
      | r = 7^2 + 8^2 + \cdots + 39^2
      | c = 
}}
{{eqn | l = \sum_{i \mathop = 7}^{56} k^2
      | r = 7^2 + 8^2 + \cdots + 56^2
      | c = 
}}
{{eqn | l = \sum_{i \mathop = 7}^{190} k^2
      | r = 7^2 + 8^2 + \cdots + 190^2
      | c = 
}}
{{end-eqn}}

Proof:
From Sum of Sequence of Squares:
{{:Sum of Sequence of Squares}}
Thus:
{{begin-eqn}}
{{eqn | l = \sum_{i \mathop = 7}^{29} i^2
      | r = \sum_{i \mathop = 1}^{29} i^2 - \sum_{i \mathop = 1}^6 i^2
      | c = 
}}
{{eqn | r = \frac {29 \left({29 + 1}\right) \left({2 \times 29 + 1}\right)} 6 - \frac {6 \left({6 + 1}\right) \left({2 \times 6 + 1}\right)} 6
      | c = 
}}
{{eqn | r = \frac {29 \times 30 \times 59} 6 - \frac {6 \times 7 \times 13} 6
      | c = 
}}
{{eqn | r = 8 \, 555 -  91
      | c = 
}}
{{eqn | r = 8 \, 464
      | c = 
}}
{{eqn | r = 92^2
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \sum_{i \mathop = 7}^{39} i^2
      | r = \sum_{i \mathop = 1}^{39} i^2 - \sum_{i \mathop = 1}^6 i^2
      | c = 
}}
{{eqn | r = \frac {39 \left({39 + 1}\right) \left({2 \times 39 + 1}\right)} 6 - \frac {6 \left({6 + 1}\right) \left({2 \times 6 + 1}\right)} 6
      | c = 
}}
{{eqn | r = \frac {39 \times 40 \times 79} 6 - \frac {6 \times 7 \times 13} 6
      | c = 
}}
{{eqn | r = 20 \, 540 -  91
      | c = 
}}
{{eqn | r = 20 \, 449
      | c = 
}}
{{eqn | r = 143^2
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \sum_{i \mathop = 7}^{56} i^2
      | r = \sum_{i \mathop = 1}^{56} i^2 - \sum_{i \mathop = 1}^6 i^2
      | c = 
}}
{{eqn | r = \frac {56 \left({56 + 1}\right) \left({2 \times 56 + 1}\right)} 6 - \frac {6 \left({6 + 1}\right) \left({2 \times 6 + 1}\right)} 6
      | c = 
}}
{{eqn | r = \frac {56 \times 57 \times 113} 6 - \frac {6 \times 7 \times 13} 6
      | c = 
}}
{{eqn | r = 60 \, 116 -  91
      | c = 
}}
{{eqn | r = 60 \, 025
      | c = 
}}
{{eqn | r = 245^2
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \sum_{i \mathop = 7}^{190} i^2
      | r = \sum_{i \mathop = 1}^{190} i^2 - \sum_{i \mathop = 1}^6 i^2
      | c = 
}}
{{eqn | r = \frac {190 \left({190 + 1}\right) \left({2 \times 190 + 1}\right)} 6 - \frac {6 \left({6 + 1}\right) \left({2 \times 6 + 1}\right)} 6
      | c = 
}}
{{eqn | r = \frac {190 \times 191 \times 381} 6 - \frac {6 \times 7 \times 13} 6
      | c = 
}}
{{eqn | r = 2 \, 304 \, 415 -  91
      | c = 
}}
{{eqn | r = 2 \, 304 \, 324
      | c = 
}}
{{eqn | r = 1 \, 518^2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Morphism from Ring with Unity to Module

Let $R$ be a ring with unity.
Let $M$ be an $R$-module.
Then for every $m \in M$ there exists a unique $R$-module morphism:
:$\psi: R \to M$
that sends $1$ to $m$.

Proof:
=== Existence ===
Let $r \in R$.
Let $\map \psi r := r m$.
This map is $R$-linear by definition of a module.
{{qed|lemma}}
Theorem: Universal Property of Free Module on Set

Let $R$ be a ring with unity.
Let $R^{\paren I}$ be the free $R$-module on $I$.
Let $M$ be an $R$-module.
Let $\family {m_i}_{i \mathop \in I}$ be a family of elements of $M$.
Then there exists a unique $R$-module morphism:
:$\Psi: R^{\paren I} \to M$
that sends the $i$th canonical basis element to $m_i$, for all $i \in I$.
Moreover:
:$\ds \map \Psi {\family {r_i}_{i \mathop \in I} } = \sum_{i \mathop \in I} r_i m_i$

Proof:
=== Existence ===
By Morphism from Ring with Unity to Module, for all $i$ there exists a morphism:
:$\psi_i: R \to M$
with $\map {\psi_i} 1 = m_i$.
By Universal Property of Direct Sum of Modules, there exists a morphism:
:$\Psi: R^{\paren I} \to M$
such that $\Psi \circ \iota_i = \psi_i$ for all $i$.
Thus:
:$\forall i \in I: \map \Psi {e_i} = \map \Psi {\map {\iota_i} 1} = \map {\psi_i} 1 = m_i$
We have:
:$\ds \family {r_i}_{i \mathop \in I} = \sum_{i \mathop \in I} r_i e_i$
so the expression for $\Psi$ follows by linearity.
{{qed|lemma}}
Theorem: Multiplicative Auxiliary Relation iff Images are Filtered

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a bounded below lattice.
Let $\RR$ be an auxiliary relation on $S$.
Then $\RR$ is multiplicative {{iff}}:
:for all $x \in S$: $\map \RR x$ is filtered
where $\map \RR x$ denotes the $\RR$-image of $x$.

Proof:
=== Sufficient Condition ===
Let $\RR$ be multiplicative.
Let $x \in S$.
Let $a, b \in \map \RR x$.
By definition of $\RR$-image of element:
:$\tuple {x, a}, \tuple {x, b} \in \RR$
By definition of multiplicative relation:
:$\tuple {x, a \wedge b} \in \RR$
By definition of $\RR$-image of element:
:$a \wedge b \in \map \RR x$
By Meet Precedes Operands:
:$a \wedge b \preceq a$ and $a \wedge b \preceq b$
Thus
:$\exists c \in \map \RR x: c \preceq a \land c \preceq b$
Hence $\map \RR x$ is filtered.
{{qed|lemma}}
Theorem: Characterisation of Spanning Set through Free Module Indexed by Set

Let $M$ be a unitary $R$-module.
Let $S = \family {m_i}_{i \mathop \in I}$ be a family of elements of $M$.
Let $\Psi: R^{\paren I} \to M$ be the morphism given by Universal Property of Free Module Indexed by Set.
Then $S$ is a spanning set of $M$ {{iff}} $\Psi$ is surjective.

Proof:
{{MissingLinks|linear combination}}
For $\family {r_i}_{i \mathop \in I} \in R^{\paren I}$ we have:
:$\map \Psi {\family {r_i}_{i \mathop \in I} } = \ds \sum_{i \mathop \in I} m_i r_i$
Thus $\Psi$ is surjective {{iff}} every element of $M$ is a linear combination of $S$.
{{qed}}
Category:Module Theory
htzgah8boo1b4rbklares5zk51dt0ak
Theorem: Characterisation of Linearly Independent Set through Free Module Indexed by Set

Let $M$ be a unitary $R$-module.
Let $S = \family {m_i}_{i \mathop \in I}$ be a family of elements of $M$.
Let $\Psi : R^{\paren I} \to M$ be the module homomorphism given by Universal Property of Free Module on Set.
{{TFAE}}
{{begin-itemize}}
{{item|(1):|$S$ linearly independent}}
{{item|(2):|$\Psi$ is injective}}
{{end-itemize}}

Proof:
We have:
:$\map \Psi {\family {r_i}_{i \mathop \in I} } = 0$
{{iff}}:
:$\ds \sum_{i \mathop \in I} r_i m_i = 0$
{{explain|Justify the above statement.}}
Thus  injectivity and linearly independent are equivalent.
{{explain|Justify the above statement.}}
{{qed}}
Category:Module Theory
fzdwqw7uhtlv1j4xuiti9isb1b9oab9
Theorem: Free Module is Isomorphic to Free Module on Set

Let $M$ be a unitary $R$-module.
Let $\BB = \family {b_i}_{i \mathop \in I}$ be a family of elements of $M$.
Let $\Psi: R^{\paren I} \to M$ be the morphism given by Universal Property of Free Module on Set.
{{TFAE}}
{{begin-itemize}}
{{item|(1):|$\BB$ is a basis of $M$}}
{{item|(2):|$\Psi$ is an isomorphism}}
{{end-itemize}}

Proof:
Follows directly from:
:Characterisation of Linearly Independent Set through Free Module Indexed by Set
:Characterisation of Spanning Set through Free Module Indexed by Set.
{{qed}}
Category:Free Modules
Category:Module Theory
ajf3mybiohgd4pj9cxrm4lzggyg36t6
Theorem: Direct Product of Modules is Module

Let $R$ be a ring.
Let $\family {\struct {M_i, +_i, \circ_i} }_{i \mathop \in I}$ be a family of $R$-modules.
Let $\struct {M, +, \circ}$ be their direct product.
Then $\struct {M, +, \circ}$ is a module.

Proof:
From External Direct Product of Abelian Groups is Abelian Group it follows that $(M,+)$ is an abelian group.
We need to show that:
$\forall x, y, \in M, \forall \lambda, \mu \in R$:
: $(1): \quad \lambda \circ \paren {x + y} = \paren {\lambda \circ x} + \paren {\lambda \circ y}$
: $(2): \quad \paren {\lambda +_R \mu} \circ x = \paren {\lambda \circ x} + \paren {\mu \circ x}$
: $(3): \quad \paren {\lambda \times_R \mu} \circ x = \lambda \circ \paren {\mu \circ x}$
Checking the criteria in order:
Theorem: Direct Product of Modules is Module

Let $R$ be a ring.
Let $\family {\struct {M_i, +_i, \circ_i} }_{i \mathop \in I}$ be a family of $R$-modules.
Let $\struct {M, +, \circ}$ be their direct product.
Then $\struct {M, +, \circ}$ is a module.

Proof:
This is a special case of Direct Product of Modules is Module.
Theorem: Direct Product of Unitary Modules is Unitary Module

Let $R$ be a ring with unity whose unity is $1_R$.
Let $\family {\struct {M_i, +_i, \circ_i} }_{i \mathop \in I}$ be a family of unitary $R$-modules.
Let $\struct {M, +, \circ}$ be their direct product.
Then $\struct {M, +, \circ}$ is a unitary $R$-module.

Proof:
From Direct Product of Modules is Module, $M$ is an $R$-module.
It remains to verify that:
:$\forall x \in M: 1_R \circ x = x$
By the definition of direct product, $\circ$ is a ring action induced on $M$ by $\family {\circ_i}_{i \mathop \in I}$:
:$\forall r \in R: r \circ \family {m_i}_{i \mathop \in I} = \family {r \circ_i m_i}_{i \mathop \in I}$.
We have:
{{begin-eqn}}
{{eqn | q = \exists 1_R \in R, \forall \family {m_i}_{i \mathop \in I} \in M
      | l = 1_R \circ \family {m_i}_{i \mathop \in I}
      | r = \family {1_R \circ_i m_i}_{i \mathop \in I}
      | c = {{Defof|Left Linear Ring Action}}
}}
{{eqn | r = \family {m_i}_{i \mathop \in I}
      | c = {{Module-axiom|4}}
}}
{{end-eqn}}
{{qed}}
Category:Module Theory
Category:Direct Products
7sm88b42caltcuuxb124zw3wbnljiu8
Theorem: Direct Product of Unitary Modules is Unitary Module

Let $R$ be a ring with unity whose unity is $1_R$.
Let $\family {\struct {M_i, +_i, \circ_i} }_{i \mathop \in I}$ be a family of unitary $R$-modules.
Let $\struct {M, +, \circ}$ be their direct product.
Then $\struct {M, +, \circ}$ is a unitary $R$-module.

Proof:
This is a special case of Direct Product of Unitary Modules is Unitary Module.
Theorem: Direct Product of Unitary Modules is Unitary Module

Let $R$ be a ring with unity whose unity is $1_R$.
Let $\family {\struct {M_i, +_i, \circ_i} }_{i \mathop \in I}$ be a family of unitary $R$-modules.
Let $\struct {M, +, \circ}$ be their direct product.
Then $\struct {M, +, \circ}$ is a unitary $R$-module.

Proof:
From Finite Direct Product of Modules is Module we have that $G$ is a module.
It remains to be shown that:
:$\forall x \in G: 1_R \circ x = x$
Let $x = \tuple {x_1, x_2, \ldots, x_n} \in G$.
Then:
{{begin-eqn}}
{{eqn | l = 1_R \circ x
      | r = 1_R \circ \tuple {x_1, x_2, \ldots, x_n}
      | c = 
}}
{{eqn | r = \tuple {1_R \circ x_1, 1_R \circ x_2, \ldots, 1_R \circ x_n}
      | c = 
}}
{{eqn | r = \tuple {x_1, x_2, \ldots, x_n}
      | c = 
}}
{{eqn | r = x
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Auxiliary Relation Image of Element is Upper Section

Let $L = \struct {S, \preceq}$ be an ordered set.
Let $R$ be an auxiliary relation on $S$.
Let $x \in S$.
Then $\map R x$ is an upper section
where $\map R x$ denotes the image of $x$ under $R$.

Proof:
Let $a \in \map R x, b \in S$ such that
:$a \preceq b$
By definition of $R$-image of element:
:$\tuple {x, a} \in R$
By definition of reflexivity:
:$x \preceq x$
By definition of auxiliary relation:
:$\tuple {x, b} \in R$
Thus by definition of $R$-image of element:
:$b \in \map R x$
{{qed}}
Theorem: Multiplicative Auxiliary Relation iff Congruent

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a bounded below lattice.
Let $\RR$ be an auxiliary relation on $S$.
Then $\RR$ is multiplicative {{iff}}:
:$\forall a, b, x, y \in S: \tuple {a, x}, \tuple {b, y} \in \RR \implies \tuple {a \wedge b, x \wedge y} \in \RR$
That is {{iff}} $\RR$ is a congruence relation for $\wedge$.

Proof:
=== Sufficient Condition ===
Let $\RR$ be multiplicative.
Let $a, b, x, y \in S$ such that
:$\tuple {a, x}, \tuple {b, y} \in \RR$
By Meet Precedes Operands:
:$a \wedge b \preceq a$ and $a \wedge b \preceq b$
By definition of reflexivity:
:$x \preceq x$ and $y \preceq y$
By definition of auxiliary relation:
:$\tuple {a \wedge b, x}, \tuple {a \wedge b, y} \in \RR$
Thus by definition of multiplicative relation:
:$\tuple {a \wedge b, x \wedge y} \in \RR$
{{qed|lemma}}
Theorem: Cube which is One Less than a Square

$8$ is the only cube number which is $1$ less than a square:
:$2^3 + 1 = 3^2$

Proof:
This is a specific instance of 1 plus Perfect Power is not Prime Power except for 9.
{{qed}}
Theorem: Prime Powers Differing by One

$8$ and $9$ are the only powers of prime numbers which differ by exactly $1$:
:$2^3 + 1 = 3^2$

Proof:
This is a direct consequence of 1 plus Perfect Power is not Prime Power except for 9.
{{qed}}
Theorem: Monoid Ring of Commutative Monoid over Commutative Ring is Commutative

Let $R$ be a commutative ring.
Let $G$ be a commutative monoid.
Let $\sqbrk R G$ be the monoid ring of $G$ over $R$.
Then $\sqbrk R G$ is commutative.

Proof:
{{proof wanted}}
Category:Commutative Monoids
Category:Commutative Rings
d4keyldaa78pzil8a5k8ky59lhnxm9a
Theorem: 3 Non-Parallel Planes divide Space into 8

Let $3$ planes which are pairwise non-parallel be constructed in ordinary $3$-dimensional space.
Then that space is divided into $8$ parts by those planes.

Proof:
{{ProofWanted|Intuitively obvious but needs a run-up<br/>It's not actually even true -- consider the case where all $3$ lines of intersection of the $3$ planes are parallel. Needs to be reworded, presumably just means the lines of intersection are pairwise non-parallel as well.}}
Theorem: Divisibility by 8

An integer $N$ expressed in decimal notation is divisible by $8$ {{iff}} the $3$ {{LSD}}s of $N$ form a $3$-digit integer divisible by $8$.
That is:
:$N = \sqbrk {a_n \ldots a_2 a_1 a_0}_{10} = a_0 + a_1 10 + a_2 10^2 + \cdots + a_n 10^n$ is divisible by $8$ 
{{iff}}:
:$100 a_2 + 10 a_1 + a_0$ is divisible by $8$.

Proof:
Let $N$ be divisible by $8$.
Then:
{{begin-eqn}}
{{eqn | l = N
      | o = \equiv
      | r = 0 \pmod 8
}}
{{eqn | ll= \leadstoandfrom
      | l = \sum_{k \mathop = 0}^n a_k 10^k
      | o = \equiv
      | r = 0 \pmod 8
}}
{{eqn | ll= \leadstoandfrom
      | l = 100 a_2 + 10 a_1 + a_0 + 10^3 \sum_{k \mathop = 3}^n a_k 10^{k - 3}
      | o = \equiv
      | r = 0 \pmod 8
}}
{{eqn | ll= \leadstoandfrom
      | l = 100 a_2 + 10 a_1 + a_0
      | o = \equiv
      | r = 0 \pmod 8
      | c = as $10^3 \equiv 0 \pmod 8$
}}
{{end-eqn}}
{{qed}}
Theorem: Closed Form for Octagonal Numbers

The closed-form expression for the $n$th octagonal number is:
:$O_n = n \paren {3 n - 2}$

Proof:
Octagonal numbers are $k$-gonal numbers where $k = 8$.
From Closed Form for Polygonal Numbers we have that:
:$\map P {k, n} = \dfrac n 2 \paren {\paren {k - 2} n - k + 4}$
Hence:
{{begin-eqn}}
{{eqn | l = O_n
      | r = \frac n 2 \paren {\paren {8 - 2} n - 8 + 4}
      | c = Closed Form for Polygonal Numbers
}}
{{eqn | r = n \paren {3 n - 2}
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: No Perfect Magic Cube of Order Less than 5 Exists

Apart from the trivial order $1$ case, no perfect magic cube exists whose order is $4$ or less.

Proof:
=== Order $2$ ===
Consider a layer of the order $2$ perfect magic cube:
:<nowiki>$\begin{array}{|c|c|}
\hline  a & b \\
\hline  c & d \\
\hline
\end{array}$</nowiki>
Then we must have $a + b = a + c$.
So $b = c$, so they are not distinct, so this array cannot be a layer of a perfect magic cube.
{{qed|lemma}}
Theorem: Modulus of Positive Real Number to Complex Power is Positive Real Number to Power of Real Part

Let $z \in \C$ be a complex number.
Let $t > 0$ be wholly real.
Let $t^z$ be $t$ to the power of $z$ defined on its principal branch.
Then:
:$\cmod {t^z} = t^{\map \Re z}$

Proof:
{{begin-eqn}}
{{eqn | l = \cmod {t^z}
      | r = \cmod {t^{\map \Re z + i \map \Im z} }
}}
{{eqn | r = \cmod {t^{\map \Re z} t^{i \map \Im z} }
      | c = Sum of Complex Indices of Real Number
}}
{{eqn | r = \cmod {t^{\map \Re z} } \cmod {t^{i \map \Im z} }
      | c = Complex Modulus of Product of Complex Numbers
}}
{{eqn | r = \cmod {t^{\map \Re z} }
      | c = Modulus of Exponential of Imaginary Number is One:Corollary
}}
{{eqn | r = t^{\map \Re z}
      | c = Power of Positive Real Number is Positive
}} 
{{end-eqn}}
{{qed}}
Category:Complex Modulus
Category:Complex Analysis
ix6871u9khqhoqtc8e7ei0pqor9yd6y
Theorem: Characterization of Pseudoprime Element when Way Below Relation is Multiplicative

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a bounded below continuous lattice such that
:$\ll$ is multiplicative relation
where $\ll$ denotes the way below relation of $L$.
Let $p \in S$.
Then $p$ is pseudoprime element {{iff}}
:$\forall a, b \in S: a \wedge b \ll p \implies a \preceq p \lor b \preceq p$

Proof:
=== Sufficient Condition ===
Let $p$ be pseudoprime element.
Let $a, b \in S$ such that
:$a \wedge b \ll p$
By definition of meet:
:$\inf \left\{ {a, b}\right\} \ll p$
By Characterization of Pseudoprime Element by Finite Infima:
:$\exists c \in \left\{ {a, b}\right\}: c \preceq p$
Thus
:$a \preceq p$ or $b \preceq p$
{{qed|lemma}}
Theorem: Number of Distinct Deltahedra is Unlimited

There are an unlimited number of distinct deltahedra.

Proof:
To any deltahedron, it is possible to attach a regular tetrahedron to any of its faces to create a new deltahedron with $2$ more faces.
Theorem: Way Below Relation is Multiplicative implies Pseudoprime Element is Prime

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a bounded below continuous lattice such that
:$\ll$ is multiplicative relation
where $\ll$ denotes the way below relation of $L$.
Let $p \in S$.
Then $p$ is a pseudoprime element is a prime element.

Proof:
Let $p$ be a pseudoprime element.
{{AimForCont}}:
:$p$ is not a prime element.
By definition of prime element:
:$\exists x, y \in S: x \wedge y \preceq p$ and $x \npreceq p$ and $y \npreceq p$
By definition of continuous:
:$\forall z \in S: z^\ll$ is directed.
and
:$L$ satisfies the axiom of approximation.
By Axiom of Approximation in Up-Complete Semilattice:
:$\exists u \in S: u \ll x \land u \npreceq p$
and
:$\exists v \in S: v \ll y \land v \npreceq p$
By Way Below Relation is Auxiliary Relation:
:$\ll$ is auxiliary relation.
By Multiplicative Auxiliary Relation iff Congruent:
:$u \wedge v \ll x \wedge y$
By definition of transitivity:
:$u \wedge v \ll p$
By Characterization of Pseudoprime Element when Way Below Relation is Multiplicative:
:$u \preceq p$ or $v \preceq p$
This contradicts $u \npreceq p$ and $v \npreceq p$
{{qed}}
Theorem: If Every Element Pseudoprime is Prime then Way Below Relation is Multiplicative

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a bounded below continuous distributive lattice.
Let every element $p \in S$: $p$ is pseudoprime $\implies p$ is prime.
Then $\ll$ is multiplicative
where $\ll$ denotes the way below relation of $L$.

Proof:
Let $a, x, y \in S$ such that:
:$a \ll x$ and $a \ll y$
{{AimForCont}}:
:$a \not\ll x \wedge y$
We will prove that:
:$\forall z \in S: z \in \paren {x \wedge y}^\ll \implies z \notin a^\succeq$
Let $z \in S$ such that:
:$z \in \paren {x \wedge y}^\ll$
By definition of way below closure:
:$z \ll x \wedge y$
{{AimForCont}}:
:$z \in a^\succeq$
By definition of upper closure of element:
:$a \preceq z$
By Preceding and Way Below implies Way Below:
:$a \ll x \wedge y$
This contradicts $a \not\ll x \wedge y$
{{qed|lemma}}
By definitions of empty set and intersection:
:$\paren {x \wedge y}^\ll \cap a^\succeq = \O$
By Way Below Closure is Ideal in Bounded Below Join Semilattice:
:$\paren {x \wedge y}^\ll$ is ideal in $L$.
By Upper Closure of Element is Filter:
:$a^\succeq$ is filter on $L$.
By If Ideal and Filter are Disjoint then There Exists Prime Ideal Including Ideal and Disjoint from Filter:
:there exists prime ideal $P$ in $L$:
:$\paren {x \wedge y}^\ll \subseteq P$ and $P \cap a^\succeq = \O$
By definition of pseudoprime element:
:$\sup P$ is pseudoprime.
By assumption:
:$\sup P$ is prime.
By definition of reflexivity:
:$a \preceq a$
By definition of upper closure of element:
:$a \in a^\succeq$
By the axiom of approximation:
:$\sup \paren {x \wedge y}^\ll = x \wedge y$
By definition of up-complete:
:$\paren {x \wedge y}^\ll$ admits a supremum
and
:$P$ admits a supremum.
By Supremum of Subset:
:$x \wedge y \preceq \sup P$
By definition of prime element:
:$x \preceq \sup P$ or $y \preceq \sup P$
By Way Below iff Second Operand Preceding Supremum of Ideal implies First Operand is Element of Ideal:
:$a \in P$
By definition of intersection:
:$a \in P \cap a^\succeq$
This contradicts $P \cap a^\succeq = \O$
{{qed}}
Theorem: Upper Closure of Element is Way Below Open Filter iff Element is Compact

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a complete lattice.
Let $x \in S$.
Then:
:$x^\succeq$ is a way below open filter on $L$
{{iff}}
:$x$ is compact

Proof:
=== Sufficient Condition ===
Suppose:
:$x^\succeq$ is a way below open filter on $L$
By definitions of upper closure of element and reflexivity:
:$x \in x^\succeq$
By definition of way below open:
:$\exists y \in x^\succeq: y \ll x$
By definition of upper closure of element:
:$x \preceq y$
By Preceding and Way Below implies Way Below and definition of reflexivity:
:$x \ll x$
By definition:
:$x$ is compact.
{{qed|lemma}}
Theorem: 9 is Only Square which is Sum of 2 Consecutive Positive Cubes

Discounting the trivial solution:
:$1^2 = 1 = 0^3 + 1^3$
$9$ is the only square number which is the sum of $2$ consecutive positive cube numbers:
:$3^2 = 9 = 1^3 + 2^3$

Proof:
The expression for the $n$th square number is:
:$n^2$
for $n \in \Z$.
The expression for the $n$th cube number is:
:$n^3$
again, for $n \in \Z$.
Therefore the closed-form expression for the $n$th sum of two consecutive cubes is:
:$n^3 + \paren {n + 1}^3$
This simplifies by {{Corollary|Cube of Sum}} to:
:$2 n^3 + 3 n^2 + 3 n + 1$
Equate the two expressions with a variable replacing $n$:
{{begin-eqn}}
{{eqn | l = y^2
      | r = 2 x^3 + 3 x^2 + 3 x + 1
      | c =
}}
{{eqn | ll= \leadsto
      | l = 4 y^2
      | r = 8 x^3 + 12 x^2 + 12 x + 4
      | c =
}}
{{eqn | ll= \leadsto
      | l = \paren {2 y}^2
      | r = \paren {2 x}^3 + 3 \paren {4 x^2 + 4 x + 1} + 1
      | c =
}}
{{eqn | r = \paren {2 x}^3 + 1^3 + 3 \paren {2 x + 1}^2
      | c =
}}
{{eqn | r = \paren {2 x + 1} \paren { \paren {2 x}^2 -2 x + 1} + 3 \paren {2 x + 1}^2
      | c =
}}
{{eqn | r = \paren {2 x + 1} \paren { \paren {2 x}^2 -2 x + 1 + 3 \paren {2 x + 1} }
      | c =
}}
{{eqn | r = \paren {2 x + 1} \paren {4 x^2 + 4x + 1 + 3 }
      | c =
}}
{{eqn | r = \paren {2 x + 1} \paren {\paren {2x + 1}^2 + 3}
      | c =
}}
{{end-eqn}}
Substituting:
:$u = 2 x + 1$
:$v = 2 y$
the equation becomes:
:$v^2 = u^3 + 3 u$
We then apply Integral Points of Elliptic Curve $y^2 = x^3 + 3 x$:
{{:Integral Points of Elliptic Curve y^2 = x^3+3x}}
We then write them in terms of $x$ and $y$:
:$\tuple {-\frac 1 2, 0}, \tuple {0, \pm 1}, \tuple {1, \pm 3}, \tuple {\frac {11} 2, \pm 21}$
Due to the restrictions on the variables, solutions with non-integer inputs are invalid.
This leaves $4$ solutions:
:$\tuple {0, \pm 1}, \tuple {1, \pm 3}$
as follows:
:$\paren {\pm1}^2 = 1 = 0^3 + 1^3$
:$\paren {\pm3}^2 = 9  = 1^3 + 2^3$
{{qed}}