avewright/proofwiki-math huggingface dataset:
Theorem: Irreducible Subspace is Contained in Irreducible Component

Let $T = \struct {S_1, \tau}$ be a non-empty topological space.
Let $S_2$ be an irreducible subset of $S_1$.
Then there exists an irreducible component $S_3$ of $T$ such that $S_2 \subseteq S_3$.

Proof:
By definition, an irreducible component of $X$ is an irreducible subspace that is maximal among the irreducible subspaces, ordered by the subset relation.
Consider the ordered set $\struct {\AA, \subseteq}$, where:
:$\AA := \leftset {S : S}$ is an irreducible subset of $S_1$ such that $\rightset {S_2 \subseteq S}$
We need to show that $\AA$ has a maximal element.
As $S_2 \in \AA$, we have $\AA \ne \O$.
Thus, in view of Zorn's Lemma, it suffices to show:
:each non-empty chain in $\AA$ has an upper bound in $\AA$.
Let $C$ be a non-empty chain in $\AA$.
Let:
:$M := \bigcup C$
We now show that $M$ is an upper bound of $C$.
By construction of $M$, it suffices to show:
:$M \in \AA$
As $C \subseteq \AA$, we have:
:$S_2 \subseteq M$
So, if remains to show that $M$ is an irreducible subset of $S_1$.
Let $U, V$ are non-empty open sets of $\struct {M, \tau_M}$.
In view of the definition of irreducible space, we need to show:
:$U \cap V \ne \O$
By definition of $\tau_M$, there are $U_1, V_1 \in \tau$ such that:
:$U = U_1 \cap M$
and:
:$V = V_1 \cap M$
Since:
:$\bigcup _{N \in C} \paren {U_1 \cap N} = U_1 \cap M \ne \O$
there exists $N_U \in C$ such that:
:$U_1 \cap N_U \ne \O$
Similarly, there exists $N_V \in C$ such that:
:$V_1 \cap N_V \ne \O$
As $C$ is a chain, we have either:
:$N_U \subseteq N_V$ or $N_V \subseteq N_U$
{{WLOG}}, suppose:
:$N_U \subseteq N_V$
Let:
:$U' := U_1 \cap N_V$
and:
:$V' := V_1 \cap N_V$
Then $U', V'$ are non-empty open sets of $N_V$.
Since $N_V$ is irreducible, we have:
:$U' \cap V' \ne \O$
This implies:
:$U \cap V \ne \O$
{{qed}}
{{AoC|Zorn's Lemma}}
Theorem: Irreducible Component is Closed

Let $T = \left({S, \tau}\right)$ be a topological space.
Let $Y$ be an irreducible component of $T$.
Then $Y$ is closed in $T$.

Proof:
By Closure of Irreducible Subspace is Irreducible, the closure $Y^-$ of $Y$ is irreducible.
By Set is Subset of its Topological Closure, $Y \subseteq Y^-$.
Because $Y$ is an irreducible component, we must have $Y =  Y^-$.
By Set is Closed iff Equals Topological Closure, $Y$ is closed in $T$.
{{qed}}
Category:Irreducible Spaces
dvy1gqm6tfj4oxod4zhdp6w2xxyuy5k
Theorem: Trivial Topological Space is Irreducible

Let $T = \struct {\set s, \tau}$ be a trivial topological space.
Then $T$ is irreducible.

Proof:
Follows from:
:Trivial Topological Space is Indiscrete
:Indiscrete Space is Irreducible
{{qed}}
Category:Trivial Topological Spaces
Category:Examples of Irreducible Spaces
3a8y3rju7miq9v5j6w9uyrlsu1keece
Theorem: Irreducible Components of Hausdorff Space are Points

Let $T = \struct {S, \tau}$ be a non-empty Hausdorff space.
Then the irreducible components of $T$ are the singleton sets.

Proof:
By Subspace of Hausdorff Space is Hausdorff, the irreducible components of $T$ are also Hausdorff.
By Irreducible Hausdorff Space is Singleton, they can only be singletons.
By Trivial Topological Space is Irreducible, every singleton of $X$ is indeed irreducible.
{{qed}}
Category:Irreducible Spaces
i1l3tsylbrye0j3zoedyz7d3vl9odly
Theorem: Pandigital Integer Formed by Digits in Alphabetical Order

The number $8 \, 549 \, 176 \, 320$ is the pandigital integer formed from the digits from $0$ to $9$ arranged in alphabetical order.

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = 8
      | c = eight
}}
{{eqn | o = 
      | r = 5
      | c = five
}}
{{eqn | o = 
      | r = 4
      | c = four
}}
{{eqn | o = 
      | r = 9
      | c = nine
}}
{{eqn | o = 
      | r = 1
      | c = one
}}
{{eqn | o = 
      | r = 7
      | c = seven
}}
{{eqn | o = 
      | r = 6
      | c = six
}}
{{eqn | o = 
      | r = 3
      | c = three
}}
{{eqn | o = 
      | r = 2
      | c = two
}}
{{eqn | o = 
      | r = 0
      | c = zero
}}
{{end-eqn}}
{{qed}}
Theorem: Palindromic Cube with Non-Palindromic Root

The only known palindromic cube with a root that is not itself palindromic is $10 \, 662 \, 526 \, 601$.

Proof:
We have that:
:$10 \, 662 \, 526 \, 601 = 2201^3$
There are no others whose cube root is below $10^{15}$.
Theorem: Open Set of Irreducible Space is Irreducible

Let $T = \struct {S, \tau}$ be an irreducible topological space.
Let $U$ be a non-empty open set of $T$.
Then $U$ is irreducible in its induced subspace topology.

Proof:
Let $T = \struct {S, \tau}$ be an irreducible topological space.
Let $U$ be a non-empty open set of $T$.
{{AimForCont}} $U$ is not irreducible in $T$.
Then $U = V_1 \cup V_2$ for some closed sets $V_1$ and $V_2$ of $\struct {U, \tau_U}$.
By definition of subspace topology:
:$V_1 = U \cap W_1$
and:
:$V_2 = U \cap W_2$
for some closed sets $W_1$ and $W_2$ of $T$.
Because $W_1 = S \implies V_1 = U \cap W_1 = U$, it follows that:
:$W_1 \ne S$
This is a contradiction, because $V_1$ is a proper subset of $U$.
Now $U \ne \O$ implies that $S \setminus U$ is a proper subset of $S$ which is a closed set of $T$.
Let $W_3 := W_2 \cup \paren {S \setminus U}$.
Then $W_3$ is a closed set of $T$.
Also, $W_3 \ne S$, because otherwise $V_2 = U \cap W_2 = U \cap W_3 = U$.
Thus $S = W_1 \cup W_3$ shows that $T$ is not irreducible.
The result follows by Proof by Contradiction.
{{qed}}
Theorem: Union of Open Irreducible Non-Disjoint Subspaces is Irreducible

Let $T = \struct {S, \tau}$ be an irreducible topological space.
Let $U$ and $V$ be open irreducible subspaces of $T$.
Let their intersection $U \cap V$ be non-empty.
Then their union $U \cup V$ is an irreducible subspace of $T$.

Proof:
In view of the definition of the subspace topology $\tau_{U \cup V}$, it suffices to show that for all closed sets $A_1$ and $A_2$:
:$U \cup V \subseteq A_1 \cup A_2 \implies \exists i_0 \in \set {1, 2} : U \cup V \subseteq A_{i_0}$
To this end, let $A_1$ and $A_2$ closed sets such that:
:$U \cup V \subseteq A_1 \cup A_2$.
Then, in particular:
:$U \subseteq A_1 \cup A_2$.
Since $U$ is irreducible, we have:
:$(1):\quad \exists i_0 \in \set {1,2} : U \subseteq A_{i_0}$
In particular:
{{begin-eqn}}
{{eqn | l = V
      | o = \subseteq
      | r = \paren {V \setminus U} \cup U
}}
{{eqn | o = \subseteq
      | r = \paren {V \setminus U} \cup A_{i_0}
      | c = by $(1)$
}}
{{end-eqn}}
Thus:
:$V = \paren {V \setminus U} \cup \paren {V \cap A_{i_0} }$
Here, both $V \setminus U$ and $V \cap A_{i_0}$ are closed in $V$ with respect to the subspace topology $\tau_V$.
Since $U \cap V$ is non-empty, we have:
:$V \setminus U \subsetneq V$
That is, $V \setminus U$ is a proper subset of $V$.
Since $V$ is irreducible, $V \cap A_{i_0}$ is not a proper subset of $V$.
That is:
:$V = V \cap A_{i_0}$
Hence:
:$V \subseteq A_{i_0}$
Together with $(1)$, we conclude:
:$U \cup V \subseteq A_{i_0}$
{{qed}}
Category:Irreducible Spaces
abjhtjqd2ls1zh7k867lzjw4x0at1hw
Theorem: Closed Set of Ultraconnected Space is Ultraconnected

Let $T = \struct {S, \tau}$ be an ultraconnected topological space.
Let $F \subset S$ be a closed set in $T$.
Then $F$ is ultraconnected.

Proof:
Let $A, B$ be two non-empty closed sets in $\struct {F, \tau}$.
By Closed Set in Topological Subspace, $A, B$ are closed in $T$ as well.
By {{Defof|Ultraconnected Space}}, $A$ and $B$ are not disjoint.
Since $A$, $B$ are arbitrary, no two non-empty closed sets of $\struct {F, \tau}$ are disjoint.
Hence the result from {{Defof|Ultraconnected Space}}.
{{qed}}
Theorem: Noetherian Topological Space is Compact

Let $T = \struct {X, \tau}$ be a Noetherian topological space.
Then $T$ is compact.

Proof:
Let $\family {U_i}_{i \mathop \in I}$ be a cover of $X$.
That is:
:$\ds \bigcup_{i \mathop \in I} U_i = X$
Let $V$ be the collection of finite cover of $\family {U_i}_{i \mathop \in I}$.
{{explain|Exactly what is meant by the above? Does it mean "the set / collection of all finite covers of $X$"? If not, can it be explained? If so, is there a reason why we cannot use the word "Set" here? If not, we need to change that word "collection" to a specific link to set, and make "finite cover" plural.}}
Let $W = \set {\bigcup Y: Y \in V}$.
Then $W$ is a collection of open sets of $T$.
{{explain|Again, is there any reason to use "collection" and not "set"? Is there a possibility that $W$ is itself not a set?}}
By {{Defof|Noetherian Topological Space|index = 4}}, $W$ has a maximal element {{WRT}} the subset relation.
Let $\ds U' = \bigcup_{j \mathop = 1}^n U_{i_j}$ be the maximal element.
{{AimForCont}} $U' \subsetneq X$.
Let $x \in X \setminus U'$.
Let $U_{i_{n + 1} }$ be a neighborhood of $x$, where $i_{n + 1} \in I$.
Then $U' \cup U_{i_{n + 1} }$ is larger than $U'$.
This contradicts our hypothesis that $U'$ is maximal.
Hence $U'$ is a finite subcover.
This shows that $\struct {X, \tau}$ is compact.
{{qed}}
Theorem: Noetherian Topological Space is Compact

Let $T = \struct {X, \tau}$ be a Noetherian topological space.
Then $T$ is compact.

Proof:
{{Recall|Compact Topological Space|index = 1|compact topological space}}
{{:Definition:Compact Topological Space/Definition 1}}
We may assume $X \ne \O$, since the claim is otherwise trivial.
Let $\CC \subseteq \tau$ be an arbitrary cover for $X$.
We shall show that $\CC$ has a finite subcover.
Consider:
:$A := \leftset {\bigcup \eta: \eta}$ is a finite subset of $\rightset \CC$
$A$ has the following properties:
:$(1): \quad A \ne \O$
:$(2): \quad A \subseteq \tau$
Let $\alpha = \bigcup \eta$.
We have:
{{begin-eqn}}
{{eqn | l = \alpha
      | o = \in
      | r = A
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \forall U \in \CC
      | l = \bigcup \paren {\eta \cup \set U}
      | r = \alpha \cup U
      | c = 
}}
{{eqn | o = \in
      | r = A
      | c = 
}}
{{end-eqn}}
From $(1)$ and $(2)$, by {{Defof|Noetherian Topological Space|index = 4}}, $A$ has a maximal element $\alpha$.
We now show that:
:$\alpha = X$
{{AimForCont}}:
:$\exists x \in X \setminus \alpha$
Since $\CC$ is a cover for $X$:
:$\exists U \in \CC : x \in U$
so that:
:$\alpha \subsetneqq \alpha \cup U$
This contradicts $(3)$.
Hence by Proof by Contradiction:
:$\not \exists x \in X \setminus \alpha$
and so:
:$\alpha = X$
as required.
{{qed|lemma}}
Because $\alpha \in A$, we can write it as:
:$\alpha = U_1 \cup \cdots \cup U_n$
using $U_1, \ldots, U_n \in \CC$ for some $n \in \N_{>0}$.
This means:
:$X = U_1 \cup \cdots \cup U_n$
Therefore:
:$\set {U_1, \ldots, U_n}$ is a finite subcover of $\CC$ for $X$.
{{qed}}
Theorem: Subspace of Noetherian Topological Space is Noetherian

Let $X$ be a Noetherian topological space.
Let $Y \subseteq X$ be a subspace.
Then $Y$ is Noetherian.

Proof:
Let $Y_1 \subset Y_2 \subset \ldots \subset$ be an ascending chain of open sets in $Y$.
{{explain|If we are going to use the term "ascending chain", then we need to have a page that defines exactly that.}}
By definition of subspace topology, there exists open sets $X_1, X_2, \ldots$ such that
:$X_i \cap Y = Y_i$
for all $i$.
By taking the intersection $Z_i := \ds \bigcap_{j \mathop = i}^{\infty} X_j$, we have:
:$Z_i \cap Y = Y_i$
:$Z_1 \subset Z_2 \subset \dots$
Since $X$ is Noetherian, every ascending chain of open sets is eventually constant.
Hence $Z_i$ is eventually constant.
Then $Y_i = Z_i \cap Y$ is eventually constant.
Hence $Y$ is also Noetherian.
{{qed}}
Theorem: Zero Locus of Larger Set is Smaller

Let $k$ be a field.
Let $n \ge 1$ be a natural number.
Let $A = k \sqbrk {X_1, \ldots, X_n}$ be the ring of polynomials in $n$ variables over $k$.
Let $I, J \subseteq A$ be subsets, and $\map V I$ and $\map V J$ their zero loci.
Let $I \subseteq J$.
Then $\map V I \supseteq \map V J$.

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \map V J
}}
{{eqn | ll= \leadsto
      | q = \forall f \in J
      | l = \map f x
      | r = 0
}}
{{eqn | ll= \leadsto
      | q = \forall f \in I
      | l = \map f x
      | r = 0
      | c = since $I \subseteq J$ by assumption
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = \map V I
}}
{{end-eqn}}
{{qed}}
Category:Algebraic Geometry
iwzn7vb06xuo0gw7n8zruiub5rqx49r
Theorem: Smallest Multiply Perfect Number of Order 5

The number $14 \, 182 \, 439 \, 040$ is multiply perfect of order $5$:
:$\map {\sigma_1} {14 \, 182 \, 439 \, 040} = 70 \, 912 \, 195 \, 200 = 5 \times 14 \, 182 \, 439 \, 040$
It is the smallest positive integer to be so.

Proof:
From {{DSFLink|14,182,439,040|14 \, 182 \, 439 \, 040}}:
:$\map {\sigma_1} {14 \, 182 \, 439 \, 040} = 70 \, 912 \, 195 \, 200$
{{ProofWanted|That it is the smallest one remains to be proved.}}
Theorem: Smallest Fourth Power expressible as Sum of 4 Fourth Powers

$15 \, 527 \, 402 \, 881$ is the smallest fourth power which can be expressed as the sum of $4$ fourth powers:
:$15 \, 527 \, 402 \, 881 = 353^4 = 30^4 + 120^4 + 272^4 + 315^4$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = 30^4 + 120^4 + 272^4 + 315^4
      | c = 
}}
{{eqn | r = 810 \, 000 + 207 \, 360 \, 000 + 5 \, 473 \, 632 \, 256 + 9 \, 845 \, 600 \, 625
      | c = 
}}
{{eqn | r = 15 \, 527 \, 402 \, 881
      | c = 
}}
{{eqn | r = 353^4
      | c = 
}}
{{end-eqn}}
{{ProofWanted|That it is the smallest remains to be proved.}}
Theorem: Largest Known Lead by 4n+1 in Prime Number Race

In the prime number race between prime numbers of the form $4 n - 1$ and $4 n + 1$, the highest known stretch of integers where $4 n + 1$ is not less than $4 n - 1$ is between $18 \, 465 \, 126 \, 293$ and $19 \, 033 \, 524 \, 538$.

Proof:
First note that:
{{begin-eqn}}
{{eqn | l = 18 \, 465 \, 126 \, 257
      | r = 4 \times 4 \, 616 \, 281 \, 564 + 1
      | c = 
}}
{{eqn | l = 18 \, 465 \, 126 \, 293
      | r = 4 \times 4 \, 616 \, 281 \, 573 + 1
      | c = 
}}
{{end-eqn}}
where it can be seen that prime numbers of the form $4 n + 1$ are locally increasing, and:
{{begin-eqn}}
{{eqn | l = 19 \, 033 \, 524 \, 533
      | r = 4 \times 4 \, 758 \, 381 \, 133 + 1
      | c = 
}}
{{eqn | l = 19 \, 033 \, 524 \, 539
      | r = 4 \times 4 \, 758 \, 381 \, 135 - 1
      | c = 
}}
{{end-eqn}}
where it can be seen at that point prime numbers of the form $4 n - 1$ may now be in front, but this is inconclusive.
{{ProofWanted|I'm not actually sure this is correct. If $4 n - 1$ is now in front for the first time since $18 \, 465 \, 126 \, 293$, I would expect the previous prime also to be of the same form -- but it is not.}}
Theorem: Number whose Square is in 2 Identical Halves

The number $36 \, 363 \, 636 \, 364$ has the property that its square can be split into two identical halves:
:$36 \, 363 \, 636 \, 364 = 1 \, 322 \, 314 \, 049 \, 613 \, 223 \, 140 \, 496$

Proof:
It just does.
Theorem: Fifth Power expressible as Sum of 4 Fifth Powers

$61 \, 917 \, 364 \, 224$ can be expressed as the sum of $4$ fifth powers:
:$61 \, 917 \, 364 \, 224 = 144^5 = 27^5 + 84^5 + 110^5 + 133^5$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = 27^5 + 84^5 + 110^5 + 133^5
      | c = 
}}
{{eqn | r = 14 \, 348 \, 907 + 4 \, 182 \, 119 \, 424 + 16 \, 105 \, 100 \, 000 + 41 \, 615 \, 795 \, 893
      | c = 
}}
{{eqn | r = 61 \, 917 \, 364 \, 224
      | c = 
}}
{{eqn | r = 144^5
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Common Sum of 3 Distinct Amicable Pairs

The integer $64 \, 795 \, 852 \, 800$ is the sum of $3$ distinct amicable pairs:
:$29 \, 912 \, 035 \, 725$ and $34 \, 883 \, 817 \, 075$
:$31 \, 695 \, 652 \, 275$ and $33 \, 100 \, 200 \, 525$
:$32 \, 129 \, 958 \, 525$ and $32 \, 665 \, 894 \, 275$
all of them odd.

Proof:
We have that:
From $29 \, 912 \, 035 \, 725$ and $34 \, 883 \, 817 \, 075$ are amicable:
{{:Odd Amicable Pair/Examples/29,912,035,725-34,883,817,075}}
From $31 \, 695 \, 652 \, 275$ and $33 \, 100 \, 200 \, 525$ are amicable:
{{:Odd Amicable Pair/Examples/31,695,652,275-33,100,200,525}}
From $32 \, 129 \, 958 \, 525$ and $32 \, 665 \, 894 \, 275$ are amicable:
{{:Odd Amicable Pair/Examples/32,129,958,525-32,665,894,275}}
{{qed}}
Theorem: Probability of Receiving Complete Suit as Hand at Bridge

The probability of being dealt a complete suit in a deal at Bridge is $1$ in $158 \, 753 \, 389 \, 900$.

Proof:
{{ProofWanted|Straightforward but boring exercise in combinatorics}}
Theorem: Polynomial Ring is Generated by Indeterminate over Ground Ring

Let $R$ be a commutative ring with unity.
Let $R \sqbrk X$ be a polynomial ring over $R$.
Let $\iota: R \to R \sqbrk X$ be the embedding.
Then $R \sqbrk X$ is generated by $X$ over $R$.

Proof:
{{ProofWanted|Use Polynomial is Linear Combination of Monomials}}
Category:Polynomial Theory
2x9lzdnsljh8sd5unxy7zgtw235pu2z
Theorem: Smallest Cunningham Chain of the First Kind of Length 12

The smallest Cunningham chain of the first kind of length $12$ is:
:$554 \, 688 \, 278 \, 429$, $1 \, 109 \, 376 \, 556 \, 859$, $2 \, 218 \, 753 \, 113 \, 719$, $4 \, 437 \, 506 \, 227 \, 439$,
::$8 \, 875 \, 012 \, 454 \, 879$, $17 \, 750 \, 024 \, 909 \, 759$, $35 \, 500 \, 049 \, 819 \, 519$, $71 \, 000 \, 099 \, 639 \, 039$,
::$142 \, 000 \, 199 \, 278 \, 079$, $284 \, 000 \, 398 \, 556 \, 159$, $568 \, 000 \, 797 \, 112 \, 319$, $1 \, 136 \, 001 \, 594 \, 224 \, 639$

Proof:
Let $C$ denote the sequence in question.
We have that $554 \, 688 \, 278 \, 429$ is prime.
First note that:
:$\dfrac {554 \, 688 \, 278 \, 429 - 1} 2 = 277 \, 344 \, 139 \, 214 = 2 \times 138 \, 672 \, 069 \, 607$
and so is not prime.
Thus $554 \, 688 \, 278 \, 429$ is not a safe prime, and thus fulfils the requirement for $C$ to be a Cunningham chain of the first kind.
Then:
{{begin-eqn}}
{{eqn | n = 1
      | l = 2 \times 554 \, 688 \, 278 \, 429 + 1
      | r = 1 \, 109 \, 376 \, 556 \, 859
      | c = which is prime
}}
{{eqn | n = 2
      | l = 2 \times 1 \, 109 \, 376 \, 556 \, 859 + 1
      | r = 2 \, 218 \, 753 \, 113 \, 719
      | c = which is prime
}}
{{eqn | n = 3
      | l = 2 \times 2 \, 218 \, 753 \, 113 \, 719 + 1
      | r = 4 \, 437 \, 506 \, 227 \, 439
      | c = which is prime
}}
{{eqn | n = 4
      | l = 2 \times 4 \, 437 \, 506 \, 227 \, 439 + 1
      | r = 8 \, 875 \, 012 \, 454 \, 879
      | c = which is prime
}}
{{eqn | n = 5
      | l = 2 \times 8 \, 875 \, 012 \, 454 \, 879 + 1
      | r = 17 \, 750 \, 024 \, 909 \, 759
      | c = which is prime
}}
{{eqn | n = 6
      | l = 2 \times 17 \, 750 \, 024 \, 909 \, 759 + 1
      | r = 35 \, 500 \, 049 \, 819 \, 519
      | c = which is prime
}}
{{eqn | n = 7
      | l = 2 \times 35 \, 500 \, 049 \, 819 \, 519 + 1
      | r = 71 \, 000 \, 099 \, 639 \, 039
      | c = which is prime
}}
{{eqn | n = 8
      | l = 2 \times 71 \, 000 \, 099 \, 639 \, 039 + 1
      | r = 142 \, 000 \, 199 \, 278 \, 079
      | c = which is prime
}}
{{eqn | n = 9
      | l = 2 \times 142 \, 000 \, 199 \, 278 \, 079 + 1
      | r = 284 \, 000 \, 398 \, 556 \, 159
      | c = which is prime
}}
{{eqn | n = 10
      | l = 2 \times 284 \, 000 \, 398 \, 556 \, 159 + 1
      | r = 568 \, 000 \, 797 \, 112 \, 319
      | c = which is prime
}}
{{eqn | n = 11
      | l = 2 \times 568 \, 000 \, 797 \, 112 \, 319 + 1
      | r = 1 \, 136 \, 001 \, 594 \, 224 \, 639
      | c = which is prime
}}
{{eqn | n = 12
      | l = 2 \times 1 \, 136 \, 001 \, 594 \, 224 \, 639 + 1
      | r = 2 \, 272 \, 003 \, 188 \, 449 \, 279
      | c = which is $19 \times 119 \, 579 \, 115 \, 181 \, 541$ prime
}}
{{end-eqn}}
Establishing that this is indeed the smallest such Cunningham chain of the first kind of length $12$ can be done by a computer search.
{{qed}}
Theorem: Set of Integers Bounded Above by Real Number has Greatest Element

Let $\Z$ be the set of integers.
Let $\le$ be the usual ordering on the real numbers $\R$.
Let $\O \subset S \subseteq \Z$ such that $S$ is bounded above in $\struct {\R, \le}$.
Then $S$ has a greatest element.

Proof:
Let $S$ be bounded above by $x \in \R$.
By the Axiom of Archimedes, there exists an integer $n \ge x$.
Then $S$ is bounded above by $n$.
By Set of Integers Bounded Above by Integer has Greatest Element, $S$ has a greatest element.
{{qed}}
Theorem: Set of Integers Bounded Below by Real Number has Smallest Element

Let $\Z$ be the set of integers.
Let $\le$ be the usual ordering on the real numbers $\R$.
Let $\O \subset S \subseteq \Z$ such that $S$ is bounded below in $\struct {\R, \le}$.
Then $S$ has a smallest element.

Proof:
Let $S$ be bounded below by $x \in \R$.
By the Axiom of Archimedes, there exists an integer $n \le x$.
Then $S$ is bounded below by $n$.
By Set of Integers Bounded Below by Integer has Smallest Element, $S$ has a smallest element.
{{qed}}
Theorem: Real Number lies between Unique Pair of Consecutive Integers

Let $x$ be a real number.

Proof:
=== Existence ===
By Set of Integers Bounded Above by Real Number has Greatest Element, the set:
:$S = \left\{{m \in \Z: m \le x}\right\}$
has a greatest element, say $n$.
Because $n+1>n$, $n+1\notin S$.
Thus $n+1> x$.
Thus $n\leq x < n+1$.
{{qed|lemma}}
Theorem: Supremum of Set of Integers is Integer

Let $S \subset \Z$ be a non-empty subset of the set of integers.
Let $S$ be bounded above in the set of real numbers.
Then its supremum $\sup S$ is an integer.

Proof:
By Supremum of Set of Integers equals Greatest Element, $S$ has a greatest element $n \in \Z$, that is equals to the supremum of $S$.
{{qed}}
Theorem: Definition:Constructed Semantics/Instance 1/Rule of Idempotence

The Rule of Idempotence:
:$(p \lor p) \implies p$
is a tautology in Instance 1 of constructed semantics.

Proof:
By the definitional abbreviation for the conditional:
:$\mathbf A \implies \mathbf B =_{\text{def}} \neg \mathbf A \lor \mathbf B$
the Rule of Idempotence can be written as:
: $\neg \left({p \lor p}\right) \lor p$
This evaluates as follows:
:$\begin{array}{|cccc|c|c|} \hline
\neg & (p & \lor & p) & \lor & p \\
\hline
2 & 2 & 1 & 1 & 2 & 1 \\
1 & 2 & 2 & 2 & 2 & 2 \\
\hline
\end{array}$
{{qed}}
Category:Formal Semantics
r07evkbzlhssv5d3yrb3yass8oq8v9l
Theorem: Definition:Constructed Semantics/Instance 1/Rule of Addition

The Rule of Addition:
:$q \implies (q \lor p)$
is a tautology in Instance 1 of constructed semantics.

Proof:
By the definitional abbreviation for the conditional:
:$\mathbf A \implies \mathbf B =_{\text{def}} \neg \mathbf A \lor \mathbf B$
the Rule of Addition can be written as:
: $\neg q \lor \left({p \lor q}\right)$
This evaluates as follows:
:$\begin{array}{|cc|c|ccc|} \hline
\neg & q & \lor & (p & \lor & q) \\
\hline
2 & 1 & 2 & 1 & 1 & 1 \\
1 & 2 & 2 & 1 & 2 & 2 \\
2 & 1 & 2 & 2 & 2 & 1 \\
1 & 2 & 2 & 2 & 2 & 2 \\
\hline
\end{array}$
{{qed}}
Category:Formal Semantics
rk497e2li883lwe4k6qna1aco309ty8
Theorem: Definition:Constructed Semantics/Instance 1/Rule of Commutation

The Rule of Commutation:
:$\left({p \lor q}\right) \implies \left({q \lor p}\right)$
is a tautology in Instance 1 of constructed semantics.

Proof:
By the definitional abbreviation for the conditional:
:$\mathbf A \implies \mathbf B =_{\text{def}} \neg \mathbf A \lor \mathbf B$
the Rule of Commutation can be written as:
:$\neg \left({p \lor q}\right) \lor \left({q \lor p}\right)$
This evaluates as follows:
:$\begin{array}{|cccc|c|ccc|} \hline
\neg & (p & \lor & q) & \lor & (q & \lor & p) \\
\hline
2 & 1 & 1 & 1 & 2 & 1 & 1 & 1 \\
1 & 1 & 2 & 2 & 2 & 2 & 2 & 1 \\
1 & 2 & 2 & 1 & 2 & 1 & 2 & 2 \\
1 & 2 & 2 & 2 & 2 & 2 & 2 & 2 \\
\hline
\end{array}$
{{qed}}
Category:Formal Semantics
nhvy61sitluk232bj2i72se5qmw6xrs
Theorem: Supremum of Set of Integers equals Greatest Element

Let $S \subset \Z$ be a non-empty subset of the set of integers.
Let $S$ be bounded above in the set of real numbers $\R$.
Then $S$ has a greatest element, and it is equal to the supremum $\sup S$.

Proof:
By Set of Integers Bounded Above by Real Number has Greatest Element, $S$ has a greatest element, say $n \in S$.
By Greatest Element is Supremum, $n$ is the supremum of $S$.
{{qed}}