avewright/proofwiki-math huggingface dataset:
Theorem: Primitive Element Theorem

Let $E / F$ be a separable field extension of finite degree.
Then $E / F$ is simple: there exists $\alpha\in E$ such that $E = \map F \alpha$.

Proof:
{{tidy}}
{{MissingLinks}}
If $F$ is a finite field (equivalently $E$ is a finite field), this follows from Finite Extension of $\F_p$ is Generated By a Single Element, since the generator of $E / \F_p$ also generates $E / F$.
Next, assume $F$ is infinite.
Choose an algebraic closure $\overline F$ of $F$.
Let $\sigma_1, \dots, \sigma_n$ be all distinct embeddings of $E$ into $\overline F$ fixing $F$.
By definition 2 of separable degree,
:$n = \index E F_s$
Since $E / F$ is separable,
:$n = \index E F_s = \index E F$
Note that if $i \ne j$, then $\sigma _ i \ne \sigma _ j$, so
:$V_{ij} = \map \ker {\sigma _ i - \sigma _ j}$
is not equal to $E$.
By Vector Space over an Infinite Field is not equal to the Union of Proper Subspaces,
:$\ds \bigcup_{1\le i < j\le n} V_{ij}$
is a proper subfield of $E$,
so we can find $\alpha \in E$ with $\alpha \notin V_{ij}$ for all $i \ne j$.
It follows that $\map {\sigma_1} \alpha, \dots, \map {\sigma_n} \alpha$ are distinct,
so there are at least $n$ embeddings of $F \sqbrk \alpha$ into $\overline{F}$ fixing $F$,
so
:$\index {F \sqbrk \alpha} F_s \ge n$
but since $F \sqbrk \alpha / F$ is a subextension of $E / F$, by Subextensions of Separable Field Extension are Separable, $F \sqbrk \alpha / F$ is separable,
so
:$\index {F \sqbrk \alpha} F = \index {F \sqbrk \alpha} F_s \ge n$
On the other hand, by Tower Law,
:$\index {F \sqbrk \alpha} F \le \index E F = n$
Hence
:$\index {F \sqbrk \alpha} F = \index E F = n$
by Tower Law, this implies
:$\index E {F \sqbrk \alpha} = 1$
we conclude that $E = F \sqbrk \alpha$.
{{qed}}
Theorem: Largest Number not Expressible as Sum of Less than 32 Positive Fifth Powers

The largest positive integer which cannot be expressed as the sum of less than $32$ positive fifth powers is $466$:
:$466 = 18 \times 1^5 + 14 \times 2^5$

Proof:
{{ProofWanted|It needs to be shown that there are no larger numbers with this property.}}
Theorem: Smallest Square which is Sum of 3 Fourth Powers

The smallest positive integer whose square is the sum of $3$ fourth powers is $481$:
:$481^2 = 12^4 + 15^4 + 20^4$

Proof:
{{begin-eqn}}
{{eqn | l = 12^4 + 15^4 + 20^4
      | r = 20 \, 736 + 50 \, 625 + 160 \, 000
      | c = 
}}
{{eqn | r = 231 \, 361
      | c = 
}}
{{eqn | r = 481^2
      | c = 
}}
{{end-eqn}}
The smallest solution must be fourth powers of coprime integers, otherwise dividing by their GCD would yield a smaller solution.
By Fermat's Right Triangle Theorem, $x^4 + y^4 = z^2$ has no solutions.
Thus none of the fourth powers is $0$.
Consider the equation $x^4 + y^4 + z^4 = n^2$.
By Square Modulo 4, since fourth powers are squares, at most one of $x, y, z$ is odd.
If none of them are odd, the numbers are not coprime.
Therefore there is exactly one odd number.
{{qed|lemma}}
By Fermat's Little Theorem, for $3 \nmid a$:
:$a^2 \equiv 1 \pmod 3$
Therefore by Congruence of Powers:
:$a^4 \equiv 1^2 \equiv 1 \pmod 3$
For $3 \divides a$:
:$a^2 \equiv a^4 \equiv 0 \pmod 3$
Therefore we cannot have two of $x, y, z$ not divisible by $3$.
By our coprimality condition we cannot have $3 \divides x, y, z$.
Hence either $3 \nmid x, y, z$ or exactly one of $x, y, z$ is not divisible by $3$.
{{qed|lemma}}
Similarly, by Fermat's Little Theorem, for $5 \nmid a$:
:$a^4 \equiv 1 \pmod 5$
For $5 \divides a$:
:$a^4 \equiv 0 \pmod 5$
By Square Modulo 5:
:$a^2 \equiv 0, 1, 4 \pmod 5$
Therefore there is exactly one number not divisible by $5$.
{{qed|lemma}}
Since $\sqrt {481} < 22$, we only need to check fourth powers of numbers less than $22$, satisfying the criteria above.
Since there are exactly two multiples of $2$ and $5$ among $x, y, z$, at least one of them must be a multiple of $10$.
Suppose $5 \nmid x$, $5 \divides y$ and $10 \divides z$.
Theorem: Solutions to p^2 Divides 10^p - 10

The known prime numbers $p$ which satisfy the equation:
:$p^2 \divides \paren {10^p - 10}$
where $\divides$ denotes divisibility, are:
:$3, 487, 56 \, 598 \, 313$
{{OEIS|A045616}}

Proof:
{{ProofWanted|Some sort of computer program can be implemented, I suppose}}
Theorem: Kaprekar's Process on 3 Digit Number ends in 495

Let $n$ be a $3$-digit integer whose digits are not all the same.
Kaprekar's process, when applied to $n$, results in $495$ after no more than $6$ iterations.

Proof:
Let $n = \sqbrk {abc}_{10}$ denote a $3$-digit integer whose digits are $a, b, c$.
If $a = b = c$ then Kaprekar's process trivially results in $0$ after the first iteration.
{{WLOG}}, let $a \ge b \ge c$ but such that $a \ne c$.
By the Basis Representation Theorem:
:$n = 10^2 a + 10 b + c$
Let $n' = 10^2 a' + 10 b' + c'$ be the result of Kaprekar's process after the $1$st iteration on $n$.
We have:
{{begin-eqn}}
{{eqn | l = n'
      | r = \paren {100 a + 10 b + c} - \paren {100 c + 10 b + a}
      | c = 
}}
{{eqn | r = 100 \paren {a - c} + \paren {c - a}
      | c = 
}}
{{eqn | r = 100 \paren {a - c} - 10 + \paren {10 + c - a}
      | c = as $c < a$
}}
{{eqn | r = 100 \paren {a - c - 1} + \paren {100 - 10} + \paren {10 + c - a}
      | c = as $c < a$
}}
{{eqn | r = 10^2 \paren {a - c - 1} + 10 \times 9 + \paren {10 + c - a}
      | c = as $c < a$
}}
{{end-eqn}}
Thus we have that:
{{begin-eqn}}
{{eqn | l = a'
      | r = a - c - 1
}}
{{eqn | l = b'
      | r = 9
}}
{{eqn | l = c'
      | r = 10 + c - a
}}
{{end-eqn}}
Hence we have that:
{{begin-eqn}}
{{eqn | l = b'
      | o = \ge
      | r = a'
}}
{{eqn | l = b'
      | o = \ge
      | r = c'
}}
{{eqn | l = a' + c'
      | r = 9
}}
{{end-eqn}}
There are in fact only the following possibilities for $n'$:
{{begin-eqn}}
{{eqn | l = n'
      | r = 099
      | c = note that Kaprekar's process retains leading zeroes
}}
{{eqn | l = n'
      | r = 198
}}
{{eqn | l = n'
      | r = 297
}}
{{eqn | l = n'
      | r = 396
}}
{{eqn | l = n'
      | r = 495
}}
{{eqn | l = n'
      | r = 594
}}
{{eqn | l = n'
      | r = 693
}}
{{eqn | l = n'
      | r = 792
}}
{{eqn | l = n'
      | r = 891
}}
{{end-eqn}}
{{WLOG}} we inspect  Kaprekar's process on $198$:
{{begin-eqn}}
{{eqn | l = 099
      | o = \to
      | r = 990 - 099
      | c = 
}}
{{eqn | l = 891
      | o = \to
      | r = 981 - 189
      | c = 
}}
{{eqn | o = \to
      | r = 792
      | c = 
}}
{{eqn | o = \to
      | r = 972 - 279
      | c = 
}}
{{eqn | o = \to
      | r = 693
      | c = 
}}
{{eqn | o = \to
      | r = 963 - 369
      | c = 
}}
{{eqn | o = \to
      | r = 594
      | c = 
}}
{{eqn | o = \to
      | r = 954 - 459
      | c = 
}}
{{eqn | o = \to
      | r = 495
      | c = 
}}
{{end-eqn}}
and the result is seen to follow.
{{qed}}
Theorem: Nilpotent Elements of Commutative Ring form Ideal

Let $\struct {R, +, \circ}$ be a commutative ring whose zero is $0_R$ and whose unity is $1_R$.
The subset of nilpotent elements of $R$ form an ideal of $R$.

Proof:
Let $N$ be the subset of nilpotent elements.
Because $0_R$ is nilpotent, $0_R \in N$ and so $N$ is non-empty.
Let $x \in N$ and $a \in R$.
We have:
{{begin-eqn}}
{{eqn | q = \exists n \in \Z_{>0}
      | l = x^n
      | r = 0_R
      | c = {{Defof|Nilpotent Ring Element}}
}}
{{eqn | ll= \leadsto
      | l = a^n \circ x^n
      | r = 0_R
      | c = {{Defof|Ring Zero}}
}}
{{eqn | ll= \leadsto
      | l = \paren {a \circ x}^n
      | r = 0_R
      | c = Power of Product of Commutative Elements in Semigroup
}}
{{eqn | ll= \leadsto
      | l = a x
      | o = \in
      | r = N
      | c = Definition of $N$
}}
{{end-eqn}}
Let $x, y \in N$.
Let $x^n = 0$ and $y^m = 0$.
By the Binomial Theorem, $\paren {x - y}^p = 0$ for $p \ge n + m - 1$.
Thus $x - y \in N$.
Thus from Test for Ideal, $N$ is an ideal.
{{qed}}
Theorem: Equivalence of Definitions of Nilradical of Ring

{{TFAE|def = Nilradical of Ring}}
Let $A$ be a commutative ring.

Proof:
By Nilpotent Element is Contained in Prime Ideals, $\Nil A$ is contained in the intersection of all prime ideals.
It remains to prove the other inclusion.
Let $f \in A$ be not nilpotent.
Let $S$ be the set of ideals of $A$ that are disjoint from $\set {f^n: n \in \N}$.
By Zorn's Lemma, $S$ has a maximal element $P$.
In particular, $f \notin P$.
We want to show that $P$ is prime.
Let $a, b \in A$ with $a, b \notin P$.
Then the sums of ideals $\ideal a + P$ and $\ideal b + P$ contain $P$ strictly.
By the maximality of $P$, there exist $n, m \in \N$ with $f^n \in \ideal a + P$ and $f^m \in \ideal b + P$.
Then:
:$f^{m + n} \in \ideal {a b} + P$
Thus:
:$\ideal {a b} + P \notin S$
In particular:
:$a b \notin P$
Thus $P$ is prime, and so:
:$\ds f \notin \bigcap_{\mathfrak p \mathop \in \Spec A} \mathfrak p$
{{qed}}
{{AoC|Zorn's Lemma}}
Theorem: Algebraic Closure of Field is Unique

Let $F$ be a field.
Let $K$ and $L$ be algebraic closures of $F$.
Then $K$ and $L$ are $F$-isomorphic.

Proof:
{{ProofWanted}}
{{AoC}}
Category:Field Extensions
scjc721k2mx9ewxnymtjblmujpjd2u2
Theorem: Multiplicative Group of Galois Field is Cyclic

Let $\GF$ be a Galois field of order $q$.
Then its multiplicative group is cyclic of order $q-1$:
:$\GF^\times \cong C_{q - 1}$

Proof:
Follows immediately from Finite Multiplicative Subgroup of Field is Cyclic.
{{qed}}
Category:Galois Fields
jjwa16ge80xdni2x02rvbql2smj1753
Theorem: Automorphism Group of Complex Numbers over Real Numbers

The field extension $\C / \R$ of complex numbers $\C$ over real numbers $\R$ has automorphism group $\operatorname{Aut}$:
:$\operatorname{Aut} \paren {\C / \R} = \set {\operatorname{id}, \sigma}$
where:
:$\operatorname{id}$ denotes the identity mapping
:$\sigma$ denotes complex conjugation

Proof:
{{ProofWanted}}
Category:Field Extensions
Category:Automorphism Groups
io2w6he36rnjx693tdpc56j0fqej2i5
Theorem: Image under Inclusion Mapping

Let $X$ be a set.
Let $S \subseteq X$, $Z \subseteq S$.
Then $i_S \sqbrk Z = Z$
where
:$i_S$ denotes the inclusion mapping of $S$
:$i_S \sqbrk Z$ denotes the image of $Z$ under $i_S$.

Proof:
{{begin-eqn}}
{{eqn | l = i_S \sqbrk Z
      | r = \set {\map {i_S} z: z \in Z}
      | c = {{Defof|Image of Subset under Mapping}}
}}
{{eqn | r = \set {z: z \in Z}
      | c = {{Defof|Inclusion Mapping}}
}}
{{eqn | r = Z
      | c = {{Defof|Set Equality}}
}}
{{end-eqn}}
{{qed}}
Theorem: Limit Inferior of Inclusion Net is Supremum of Directed Subset

Let $L = \struct {S, \vee, \wedge, \preceq}$ be an up-complete lattice.
Let $D \subseteq S$ be a directed subset of $S$.
Let $\struct {D, \preceq'}$ be a directed ordered subset of $L$.
Let $i_D: D \to S$, the inclusion mapping, be a net in $S$.
Then $\liminf i_D = \sup D$

Proof:
{{Refactor|level = basic|Extract lemma}}
We will prove that:
:(lemma): $\forall j \in D: \map {\inf_L} {\map {\preceq'} j} = j$
Let $j \in D$.
By definitions of image of element and upper closure of element:
:$\map {\preceq'} j = j^{\succeq'}$
By Upper Closure in Ordered Subset is Intersection of Subset and Upper Closure:
:$j^{\succeq'} = D \cap j^\succeq$
By Intersection is Subset:
:$j^{\succeq'} \subseteq j^\succeq$
By Infimum of Subset and Infimum of Upper Closure of Element:
:$j \preceq \map {\inf_L} {\map {\preceq'} j}$
By definition of reflexivity:
:$j \preceq' j$
By definition of image of element:
:$j \in \map {\preceq'} j$
By definitions of infimum and lower bound:
:$\map {\inf_L} {\map {\preceq'} j} \preceq j$
Thus by definition of antisymmetry:
:$\map {\inf_L} {\map {\preceq'} j} = j$
{{qed|lemma}}
Thus
{{begin-eqn}}
{{eqn | l = \liminf i_D
      | r = \sup_L \set {\map {\inf_L} {i_D \sqbrk {\map {\preceq'} j} }: j \in D}
      | c = {{Defof|Limit Inferior of Net}}
}}
{{eqn | r = \sup_L \set {\map {\inf_L} {\map {\preceq'} j}: j \in D}
      | c = Image under Inclusion Mapping
}}
{{eqn | r = \sup_L \set {j: j \in D}
      | c = (lemma)
}}
{{eqn | r = \sup_L D
      | c = {{Defof|Set Equality}}
}}
{{end-eqn}}
{{qed}}
Theorem: Correspondence Between Group Actions and Permutation Representations

Let $G$ be a group.
Let $X$ be a set.
There is a one-to-one correspondence between group actions of $G$ on $X$ and permutation representations of $G$ in $X$, as follows:
Let $\phi : G \times X \to X$ be a group action.
Let $\rho : G \to \struct {\map \Gamma X, \circ}$ be a permutation representation.
The following are equivalent:
:$(1): \quad \rho$ is the permutation representation associated to $\phi$
:$(2): \quad \phi$ is the group action associated to $\rho$

Proof:
For $g\in G$, define the mapping $\phi_g : X \to X$ as:
:$\map {\phi_g} x = \map \phi {g, x}$
Then $\rho$ is the permutation representation associated to $\phi$ {{iff}}:
:$\forall g \in G : \map \rho g  = \phi_g$
By Equality of Mappings, this is equivalent to:
:$\forall g \in G : \forall x \in X : \map {\map \rho g} x = \map {\phi_g} x$
$\phi$ is the group action associated to $\rho$ {{iff}}:
:$\forall g \in G : \forall x \in X : \map \phi {g, x} = \map {\map \rho g} x$.
Because $\map {\phi_g} x = \map \phi {g, x}$, they are equivalent.
{{qed}}
Category:Group Actions
Category:Permutation Representations
mipuc77ll6tupmosr4gdryexoj12xsb
Theorem: Equivalence of Definitions of Field of Quotients

Let $D$ be an integral domain.
Let $F$ be a field.
{{TFAE|def = Field of Quotients}}

Proof:
=== 1 implies 2 ===
Let $K$ be a field such that:
:$\iota \sqbrk D \subseteq K \subseteq F$
We show that $F \subseteq K$.
Let $f \in F$.
By assumption, there exist $x, y \in D$ with $y \ne 0$ such that $f = \dfrac {\map \iota x} {\map \iota y}$.
Because $K$ is a field containing $\iota \sqbrk D$, $K$ also contains $f = \dfrac {\map \iota x} {\map \iota y}$.
Thus $F \subseteq K$.
{{qed|lemma}}
Theorem: Trivial Field Extension is Galois

Let $F$ be a field.
The trivial field extension $F / F$ is Galois.

Proof:
We shall show {{Defof|Galois Extension/Finite|Galois Extension|index=1}}.
Observe:
{{begin-eqn}}
{{eqn | l = \Gal {F / F}
      | r = \set {\sigma \in \Aut F: \forall k \in F: \map \sigma k = k}
      | c = {{Defof|Galois Group of Field Extension}}
}}
{{eqn | r = \set {I_F}
      | n = 1
}}
{{end-eqn}}
where $I_F$ denotes the identity mapping on $F$.
Therefore:
{{begin-eqn}}
{{eqn | l = \map {\operatorname{Fix}_F} {\Gal {F / F} }
      | r = \set {f \in F : \forall \sigma \in \Gal {F / F} : \map \sigma f = f}
      | c = {{Defof|Fixed Field}}
}}
{{eqn | r = \set {f \in F : \map {I_F} f = f}
      | c = by $(1)$
}}
{{eqn | r = F
}}
{{end-eqn}}
{{qed}}
Category:Galois Theory
3shlc1vu5tnnnhjct6rf2fy4jkfj8hh
Theorem: Field is Galois over Fixed Field of Automorphism Group

Let $E/F$ be a finite field extension.
Let $K = \operatorname{Fix}_E(\operatorname{Aut}(E/F))$ be the fixed field of the automorphism group of $E/F$.
Then $E/K$ is Galois.

Proof:
Follows from Closed Fields in Galois Connection for Field Extension (and does not use Fundamental Theorem of Galois Theory).
{{proof wanted}}
Category:Galois Theory
5f8c1ibg4vz9kywca8kf6h0d0lu6e4m
Theorem: Automorphism Group Acts Faithfully on Generating Set

Let $E/F$ be a field extension.
Let $\operatorname{Aut}(E/F)$ be its automorphism group.
Let $S\subset E$ be a generating set of the extension.
Let $S$ be stable under the group action of $\operatorname{Aut}(E/F)$.
Then the induced group action on $S$ is faithful.

Proof:
Let $\sigma \in \operatorname{Aut}(E/F)$ stabilize $S$.
Then $S$ is contained in the fixed field of $\sigma$.
By definition of generating set, $\sigma$ fixes $E$.
Thus $\operatorname{Aut}(E/F)$ acts faithfully.
{{qed}}
Category:Field Extensions
eqb5qxdw8htgw5zvgpeh6xkvv6l717w
Theorem: Upper Closure in Ordered Subset is Intersection of Subset and Upper Closure

Let $L = \left({S, \preceq}\right)$ be an ordered set.
Let $\left({T, \precsim}\right)$ be an ordered subset of $L$.
Let $t \in T$.
Then $t^\succsim = T \cap t^\succeq$

Proof:
By definition of ordered subset:
:$T \subseteq S$
We will prove that
:$t^\succsim \subseteq T \cap t^\succeq$
Let $x \in t^\succsim$
By definition of upper closure of element:
:$x \in T$ and $t \precsim x$
By definition of ordered subset:
:$t \preceq x$
By definition of upper closure of element:
:$x \in t^\succeq$
Thus by definition of intersection:
:$x \in T \cap t^\succeq$
{{qed|lemma}}
We will prove that
:$T \cap t^\succeq \subseteq t^\succsim$
Let $x \in T \cap t^\succeq$
By definition of intersection:
:$x \in T$ and $x \in t^\succeq$
By definition of upper closure of element:
:$t \preceq x$
By definition of ordered subset:
:$t \precsim x$
Thus by definition of upper closure of element:
:$x \in t^\succsim$
{{qed|lemma}}
By definition of set equality:
:$t^\succsim = T \cap t^\succeq$
{{qed}}
Category:Upper Closures
kb3ltlc37a3kdtoi35lw7nsmwueduh2
Theorem: Approximation to Power of 7 by Power of 10

:$7^{510} \approx 1 \cdotp 00000 \, 09377 \, 76536 \ldots \times 10^{431}$
This is the closest known approximation of a power of $7$ by a power of $10$.

Proof:
An intuition is given as follows:
Suppose for some $m, n \in \N$:
:$7^m = c \cdot 10^n$, where $c$ is very close to $1$.
Taking common logarithm:
:$m \log 7 = \log c + n$
Which leads to:
:$\log 7 = \dfrac n m + \dfrac {\log c} m$
where $\dfrac {\log c} m$ is very close to $0$.
To make a good approximation is to minimize $\size {\log c}$.
One may calculate the continued fraction of $\log 7$.
We use continued fractions because Convergents are Best Approximations.
One obtains $\sqbrk {0; 1, 5, 2, 5, 6, 1, 4813, 1, 1, 2, 2, \dots}$.
{{OEIS|A082571}}
Let $\dfrac {p_n} {q_n}$ be the convergent $\sqbrk {0; a_1, \dots, a_n}$.
Then:
{{begin-eqn}}
{{eqn | l = \size {\log c}
      | r = q_k \size {\log 7 - \frac {p_k} {q_k} }
}}
{{eqn | o = <
      | r = q_k \paren {\frac 1 {q_k q_{k + 1} } }
      | c = Accuracy of Convergents of Continued Fraction
}}
{{eqn | r = \frac 1 {q_{k + 1} }
}}
{{eqn | r = \frac 1 {a_{k + 1} q_k + q_{k - 1} }
      | c = Recursive Definition of Denominators of Convergents
}}
{{end-eqn}}
Thus, at least intuitively, the larger the value of the next $a_i$, the smaller $\size {\log c}$ is.
{{finish|I am not familiar with this, this is just some justification}}
$4813$ is the largest number in the expansion among at least the first $100$ numbers.
Note that $\sqbrk {0; 1, 5, 2, 5, 6, 1} = \dfrac {431} {510}$
This gives the estimate $7^{510} \approx 10^{431}$.
{{qed}}
Theorem: Limit Inferior of Repetition Net

Let $L = \struct {S, \wedge, \preceq}$ be a meet semilattice.
Let $N = \struct {\N, \le}$ be a directed ordered set.
Let $a, b \in S$.
Let $f = \sequence {c_i}_{i \mathop \in \N} = \tuple {a, b, a, b, \dots}: \N \to S$ be a net.
Then $\liminf \sequence {c_i}_{i \mathop \in \N} = a \wedge b$

Proof:
{{refactor|Make this a lemma page|level = basic}}
We will prove that
:(lemma): $\forall j \in \N: f \sqbrk {\le \paren j} = \set {a, b}$
Let $j \in \N$.
Let $x \in S$.
Assume:
:$x \in f \sqbrk {\le \paren j}$
By definition of image of set:
:$\exists i \in \le \paren j: x = \map f i$
By definition of $f$:
:$x = a$ or $x = b$
Thus by definition of unordered tuple:
:$x \in \set {a, b}$
{{qed|lemma}}
Assume:
:$x \in \set {a, b}$
We have:
:$j \le j$ and $j \le j+1$
By definition of image of element:
:$j, j + 1 \in \le \paren j$
By definition of $f$:
:$\set {\map f j, \map f {j + 1} } = \set {a, b}$
By definition of image of set:
:$\map f j, \map f {j + 1} \in f \sqbrk {\le \paren j}$
Thus by definition of unordered tuple:
$x \in f \sqbrk {\le \paren j}$
{{qed|lemma}}
Thus by definition of set equality:
:$f \sqbrk {\le \paren j} = \set {a, b}$
{{qed|lemma}}
Thus:
{{begin-eqn}}
{{eqn | l = \liminf \sequence {c_i}_{i \mathop \in \N}
| r = \sup \set {\map \inf {f \sqbrk {\mathord \le \paren j} }: j \in \N}
| c = {{Defof|Limit Inferior of Net}}
}}
{{eqn | r = \sup \set {\inf \set {a, b}: j \in \N}
| c = (lemma)
}}
{{eqn | r = \sup \set {a \wedge b: j \in \N}
| c = {{Defof|Meet (Order Theory)|meet}}
}}
{{eqn | r = a \wedge b
| c = Supremum of Singleton
}}
{{end-eqn}}
{{qed}}
Theorem: Mapping at Limit Inferior Precedes Limit Inferior of Composition Mapping and Sequence implies Mapping is Increasing

Let $\struct {S, \vee_1, \wedge_1, \preceq_1}$ and $\struct {T, \vee_2, \wedge_2, \preceq_2}$ be lattices.
Let $f: S \to T$ be a mapping such that:
:for all directed set $\struct {D, \precsim}$ and nets $N:D \to S$ in $S$: $\map f {\liminf N} \preceq_2 \map \liminf {f \circ N}$
Then $f$ is an increasing mapping.

Proof:
Let $a, b \in S$ such that
:$a \preceq_1 b$
Define $M = \struct {\N, \le}$ being an ordered set.
We will prove that:
:$M$ is a directed set.
Let $x, y \in \N$.
Thus by definition of max operation:
:$\max \set {x, y} \in \N$
Thus by definition of max operation:
:$x \le \max \set {x, y}$ and $y \le \max \set {x, y}$
{{qed|lemma}}
Define $g = \sequence {c_i}_{i \mathop \in \N} = \tuple {a, b, a, b, \dots}: \N \to S$ being a net in $S$.
By Limit Inferior of Repetition Net:
:$\liminf \sequence {c_i}_{i \mathop \in \N} = a \wedge_1 b$
By Preceding iff Meet equals Less Operand:
:$\map f {\liminf \sequence {c_i}_{i \mathop \in \N} } = \map f a$
By definition of composition of mappings:
:$f \circ g = \sequence {\map f {c_i} }_{i \mathop \in \N} = \tuple {\map f a, \map f b, \map f a, \map f b, \dots}$
By Limit Inferior of Repetition Net:
:$\map \liminf {f \circ g} = \map f a \wedge_2 \map f b$
By assumption:
:$\map f a \preceq_2 \map f a \wedge_2 \map f b$
By Meet Precedes Operands:
:$\map f a \wedge_2 \map f b \preceq_2 \map f a$
By definition of antisymmetry:
:$\map f a = \map f a \wedge_2 \map f b$
Thus by Preceding iff Meet equals Less Operand:
:$\map f a \preceq_2 \map f b$
{{qed}}
Theorem: Mapping at Limit Inferior Precedes Limit Inferior of Composition Mapping and Sequence implies Supremum of Image is Mapping at Supremum of Directed Subset

Let $\struct {S, \vee_1, \wedge_1, \preceq_1}$ and $\struct {T, \vee_2, \wedge_2, \preceq_2}$ be up-complete lattices.
Let $f: S \to T$ be a mapping such that
:for all directed set $\struct {D, \precsim}$ and net $N: D \to S$ in $S: \map f {\liminf N} \preceq_2 \map \liminf {f \circ N}$
Let $D$ be a directed subset of $S$.
Then: 
:$\map \sup {f \sqbrk D} = \map f {\sup D}$
where $f \sqbrk D$ denotes the image of $D$ under $f$.

Proof:
By Mapping at Limit Inferior Precedes Limit Inferior of Composition Mapping and Sequence implies Mapping is Increasing:
:$f$ is an increasing mapping.
By Image of Directed Subset under Increasing Mapping is Directed:
:$f \sqbrk D$ is directed.
By definition of up-complete:
:$D$ and $f \sqbrk D$ admit suprema.
By Subset and Image Admit Suprema and Mapping is Increasing implies Supremum of Image Precedes Mapping at Supremum:
:$\map \sup {f \sqbrk D} \preceq_2 \map f {\sup D}$
By Limit Inferior of Inclusion Net is Supremum of Directed Subset:
:$\sup D = \liminf i_D$
By assumption:
:$\map f {\sup D} \preceq_2 \map \liminf {f \circ i_D}$
By Composition of Mapping and Inclusion is Restriction of Mapping:
:$f \circ i_D = f {\restriction} D$
By Limit Inferior of Restriction Net is Supremum of Image of Directed Subset:
:$\map \sup {f \sqbrk D} = \map \liminf {f \circ i_D}$
Then
:$\map f {\sup D} \preceq_2 \map \sup {f \sqbrk D}$
Thus by definition of antisymmetry:
:$\map \sup {f \sqbrk D} = \map f {\sup D}$
{{qed}}
Theorem: Prime Values of Double Factorial plus 1

Let $n!!$ denote the double factorial function.
The sequence of positive integers $n$ such that $n!! + 1$ is prime begins:
:$0, 1, 2, 518, 33 \, 416, 37 \, 310, 52 \, 608, 123 \, 998, 220 \, 502, \ldots$
{{OEIS|A080778}}

Proof:
We have that:
{{begin-eqn}}
{{eqn | l = 0!! + 1
      | r = 1 + 1
      | c = {{Defof|Double Factorial}}
}}
{{eqn | r = 2
      | c = which is prime
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = 1!! + 1
      | r = 1 + 1
      | c = {{Defof|Double Factorial}}
}}
{{eqn | r = 2
      | c = which is prime
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = 2!! + 1
      | r = 2 \times 0!! + 1
      | c = {{Defof|Double Factorial}}
}}
{{eqn | r = 2 \times 1 + 1
      | c = {{Defof|Double Factorial}}
}}
{{eqn | r = 3
      | c = which is prime
}}
{{end-eqn}}
{{ProofWanted|It remains to be shown that the other integers are the only other ones with this property. Have fun.}}