avewright/proofwiki-math huggingface dataset:
Theorem: Monomials of Polynomial Ring are Linearly Independent/One Variable

Let $R$ be a commutative ring with unity.
Let $R \sqbrk X$ be a polynomial ring in one variable $X$ over $R$.
Then the set of monomials $\set {X^k : k \in \N}$ is linearly independent.

Proof:
We consider polynomial ring over sequences in $R$:
Let $\struct {R^{\left({\N}\right)}, \oplus, \odot}$ be the underlying ring of sequences of finite support.
Recall:
:$X = \sequence {0, 1, 0, 0, \ldots}$
Observe:
{{begin-eqn}}
{{eqn | l = X^2
      | r = \sequence {0, 0, 1, 0, 0, \ldots}
}}
{{eqn | l = X^3
      | r = \sequence {0, 0, 0, 1, 0, \ldots}
}}
{{eqn | o = \cdots
}}
{{eqn | l = X^k
      | r = \sequence {\underbrace {0, \ldots, 0}_k, 1, 0, \ldots}
}}
{{eqn | o = \cdots
}}
{{end-eqn}}
More generally, for all $r \in R$ and $k \in \N$:
{{begin-eqn}}
{{eqn | l = r X^k
      | r = \map \iota r \odot \sequence {\underbrace{0,\ldots,0}_k,1,0,\ldots}
}}
{{eqn | r = \sequence {r,0,\ldots} \odot \sequence {\underbrace{0,\ldots,0}_k,1,0,\ldots}
}}
{{eqn | r = \sequence {\underbrace{0,\ldots,0}_k,r,0,\ldots}
}}
{{end-eqn}}
Now let $n \in \N$ and $r_0,\ldots,r_n \in R$ be such that:
:$r_0 + r_1 X + r_2 X^2 + \cdots + r_n X^n = 0$
That is:
{{begin-eqn}}
{{eqn | o =
      | r = \sequence {r_0,0,\ldots} \oplus \sequence {0,r_1,0,\ldots} \oplus \sequence {0,0,r_2,0,\ldots} \oplus \cdots \oplus \sequence {0,\ldots,0,r_n,0,\ldots}
}}
{{eqn | r = \sequence {r_0,r_1,r_2,\ldots,r_n,0,\ldots}
}}
{{eqn | r = \sequence {0,0,\ldots}
}}
{{end-eqn}}
Therefore:
:$r_0 = \cdots = r_n = 0$
{{qed}}
Theorem: Equivalence of Definitions of Constant Polynomial

Let $R$ be a commutative ring with unity.
Let $P\in R[x]$ be a polynomial in one variable over $R$.
{{TFAE|def = Constant Polynomial}}

Proof:
=== 1 iff 2 ===
This is by definition of coefficients and degree.
{{qed|lemma}}
Theorem: Equivalence of Definitions of Minimal Polynomial

{{TFAE|def = Minimal Polynomial}}
Let $L / K$ be a field extension.
Let $\alpha \in L$ be algebraic over $K$.

Proof:
=== 1 equals 2 ===
By Minimal Polynomial is Irreducible, it follows that the two are equal.
{{qed|lemma}}
Theorem: Nonzero Ideal of Polynomial Ring over Field has Unique Monic Generator

Let $K$ be a field.
Let $K \sqbrk x$ be the polynomial ring in one variable over $K$.
Let $I \subseteq K \sqbrk x$ be a nonzero ideal.
Then $I$ is generated by a unique monic polynomial.

Proof:
{{proof wanted}}
Category:Polynomial Rings
damy55ww2yb2hn4pb8w6udwm6porpux
Theorem: Equivalence of Definitions of Integral Element of Algebra

{{TFAE|def = Integral Element of Algebra}}
Let $A$ be a commutative ring with unity.
Let $f : A \to B$ be a commutative $A$-algebra.
Let $b\in B$.

Proof:
=== Definition 1 implies Definition 2 ===
Assume $b$ is a root of a monic polynomial in $A \sqbrk x$.
That is, there are $n \in \N_{>0}$ and $a_1, \ldots , a_{n-1} \in A$ be such that:
:$b^n + a_{n - 1} b^{n-1} + \cdots + a_1 b + a_0 = 0$
That is:
:$b^n = - a_0 - a_1 b - \cdots - a_{n-1} b^{n-1}$
Therefore $\set {1, b, \ldots , b^{n-1} }$ generates $A \sqbrk b$.
{{qed|lemma}}
Theorem: Product of Closed Sets is Closed

Let $\family {\struct {S_i, \tau_i} }_{i \mathop \in I}$ be a family of topological spaces where $I$ is an arbitrary indexing set.
Let $\ds S = \prod_{i \mathop \in I} S_i$.
Let $T = \struct {S, \TT}$ be the product space of $\family {\struct {S_i, \tau_i} }_{i \mathop \in I}$ with the product topology $\TT$.
Suppose we have an indexed family of sets $\family {C_i}_{i \mathop \in I}$, where each $C_i$ is closed in $\struct {S_i, \tau_i}$.
Then $\ds \prod_{i \mathop \in I} C_i$ is closed in $\struct {S, \TT}$.

Proof:
First note that:
{{begin-eqn}}
{{eqn | l = \prod_{i \mathop \in I} C_i
      | r = \set {x \in S : \forall i \in I, x_i \in C_i}
      | c = {{Defof|Cartesian Product}}
}}
{{eqn | r = \bigcap_{i \mathop \in I} \set {x \in S: x_i \in C_i}
}}
{{end-eqn}}
Thus by Intersection of Closed Sets is Closed in Topological Space, our result is proven if we can show that $\forall i \in I: \set {x \in S: x_i \in C_i}$ is closed in $T$.
Let $y \in I$.
We see that:
{{begin-eqn}}
{{eqn | l = S \setminus \set {x \in S: x_y \in C_y}
      | r = \set {x \in S: x_y \notin C_y}
}}
{{eqn | r = \set {x \in S: x_y \in \paren {S_y \setminus C_y} }
      | c = {{Defof|Set Complement}}
}}
{{eqn | r = \pr_y^{-1} \sqbrk {S_y \setminus C_y}
      | c = {{Defof|Projection (Mapping Theory)}}
}} 
{{end-eqn}}
Since $C_y$ is closed, $\paren {S_y \setminus C_y}$ is open in $\struct {S_y, \tau_y}$ by definition.
Thus:
:$\pr_y^{-1} \sqbrk {S_y \setminus C_y} \in \BB$
where $\BB$ is the natural sub-basis of $T$:
:$\BB = \set {\pr_i^{-1} \sqbrk U: i \in I, U \in \tau_i}$
Therefore $\pr_y^{-1} \sqbrk {S_y \setminus C_y} = S \setminus \set {x \in S: x_y \in C_y}$ is open in $T$.
This implies that $\set {x \in S: x_y \in C_y}$ must be closed in $T$ by definition.
{{qed}}
Theorem: Prime Number Formed by Concatenating Consecutive Integers down to 1

Let $N$ be an integer whose decimal representation consists of the concatenation of all the integers from a given $n$ in descending order down to $1$.
Let the $N$ that is so formed be prime.
The only $n$ less than $100$ for which this is true is $82$.
That is:
:$82 \, 818 \, 079 \, 787 \, 776 \ldots 121 \, 110 \, 987 \, 654 \, 321$
is the only prime number formed this way starting at $100$ or less.

Proof:
Can be determined by checking all numbers formed in such a way for primality.
Theorem: Naturality of Yoneda Lemma for Covariant Functors

Let $\sqbrk {\mathbf C, \mathbf {Set} }$ be the covariant functor category.
Let $\mathbf C \times \sqbrk {\mathbf C, \mathbf {Set} }$ be the product category.
Let $\mathbf C \times \sqbrk {\mathbf C, \mathbf {Set} } \to \mathbf {Set}: \tuple {A, F} \mapsto \map {\operatorname {Nat} } {h^A, F}$ be the covariant functor defined as the composition of the hom bifunctor and the product of the contravariant Yoneda functor $h^-$ and the identity functor $\operatorname{id}_{\sqbrk {\mathbf C, \mathbf {Set} } }$.
Let $\operatorname{ev} : \mathbf C \times \sqbrk {\mathbf C, \mathbf {Set} } \to \mathbf {Set}: \tuple {A, F} \mapsto \map F A$ be the functor evaluation functor.
Then $\Phi_{\tuple {A, F} } : \map {\operatorname {Nat} } {h^A, F} \to \map F A: \eta \mapsto \map {\eta_A} {\operatorname {id}_A}$ defines a natural isomorphism, where $\operatorname{id}_A$ is the identity morphism of $A$.

Proof:
By the Bijection in Yoneda Lemma for Covariant Functors, $\Phi_{\tuple {A, F} }$ is a bijection for all $\tuple {A, F}$.
Let $\tuple {f, \xi}: \tuple {A, F} \to \tuple {B, G} $ be a morphism in $\mathbf C \times \sqbrk {\mathbf C, \mathbf {Set} }$.
To prove that $\Phi$ is a natural isomorphism, it remains to prove that the following diagram commutes:
:<nowiki>$\xymatrix{
\map {\operatorname {Nat} } {h^A, F} \ar[d]^{\Phi_{\tuple {A, F} } } \ar[r]^{\map {\operatorname {Nat} } {h^f, \xi} } & \map {\operatorname {Nat} } {h^B, G} \ar[d]^{\Phi_{\tuple {B, G} } } \\
F(A) \ar[r]^{\map {\operatorname {ev} } {f, \xi} }          & \map G B}$</nowiki>
Let $\eta \in \map {\operatorname {Nat} } {h^A, F}$.
We have:
{{begin-eqn}}
{{eqn | l = \map {\paren {\map {\operatorname {ev} } {f, \xi} \circ \Phi_{\tuple {A, F} } } } \eta
      | r = \map {\map {\operatorname {ev} } {f, \xi} } {\map {\eta_A} {\operatorname {id}_A} }
      | c = 
}}
{{eqn | r = \map {\paren {\xi_B\circ \map F f} } {\map {\eta_A} {\operatorname {id}_A} }
      | c = {{Defof|Functor Evaluation Bifunctor}}
}}
{{eqn | r = \map {\paren {\xi_B \circ \eta_B \circ \map {h^A} f} } {\operatorname{id}_A}
      | c = {{Defof|Natural Transformation}}, applied to $\eta: h^A \to F$
}}
{{eqn | r = \map {\paren {\xi_B \circ \eta_B} } {f \circ \operatorname{id}_A}
      | c = {{Defof|Covariant Hom Functor}}, applied to $h^A$
}}
{{eqn | r = \map {\paren {\xi_B \circ \eta_B} } f
      | c = 
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \map {\paren {\Phi_{\tuple {B, G} } \circ \map {\operatorname {Nat} } {h^f, \xi} } } \eta
      | r = \map {\Phi_{\tuple {B, G} } } {\xi \circ \eta \circ h^f}
      | c = {{Defof|Hom Bifunctor}}
}}
{{eqn | r = \map {\paren {\xi \circ \eta \circ h^f}_B} {\operatorname{id}_B}
      | c =
}}
{{eqn | r = \map {\paren {\xi_B \circ \eta_B} } {\map {\paren {h^f}_B} {\operatorname{id}_B} }
      | c = {{Defof|Vertical Composition of Natural Transformations}}
}}
{{eqn | r = \map {\paren {\xi_B \circ \eta_B} } {\operatorname{id}_B \circ f}
      | c = {{Defof|Contravariant Yoneda Functor}}, {{Defof|Precomposition Natural Transformation}}
}}
{{eqn | r = \map {\paren {\xi_B \circ \eta_B} } f
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Alternating Even-Odd Digit Palindromic Prime

Let the notation $\paren {abc}_n$ be interpreted to mean $n$ consecutive repetitions of a string of digits $abc$ concatenated in the decimal representation of an integer.
The integer:
:$\paren {10987654321234567890}_{42} 1$
has the following properties:
: it is a palindromic prime with $841$ digits
: its digits are alternately odd and even.

Proof:
{{Alpertron-factorizer|date = $22$nd March $2022$|time = $0.4$ seconds}}
This number has $20 \times 42 + 1 = 841$ digits.
The remaining properties of this number is obvious by inspection.
{{qed}}
Theorem: Smallest Titanic Palindromic Prime

The smallest titanic prime that is also palindromic is:
:$10^{1000} + 81 \, 918 \times 10^{498} + 1$
which can be written as:
:$1 \underbrace {000 \ldots 000}_{497} 81918 \underbrace {000 \ldots 000}_{497} 1$

Proof:
{{Alpertron-factorizer|date = $6$th March $2022$|time = $1.7$ seconds}}
It remains to be demonstrated that it is the smallest such palindromic prime with $1000$ digits or more.
By 11 is Only Palindromic Prime with Even Number of Digits, there are no palindromic primes with exactly $1000$ digits.
Hence such a prime must be greater than $10^{1000}$.
We need to check all numbers of the form:
:$1 \underbrace {000 \ldots 000}_{497} abcba \underbrace {000 \ldots 000}_{497} 1$
with $\sqbrk {abc} < 819$.
Using the [https://www.alpertron.com.ar/ECM.HTM Alpertron integer factorization calculator] and the argument:
 x=0;x=x+1;x<820;10^1000+x*10^500+RevDigits(x/10+10^499,10)
it is verified that there are no primes in the range $\sqbrk {abc} < 819$.
Therefore the number above is the smallest titanic palindromic prime.
{{qed}}
Theorem: Yoneda Embedding Theorem

Let $\mathbf C$ be a locally small category.
Let $\mathbf {Set}$ be the category of sets.
Let $\sqbrk { {\mathbf C}^{\operatorname {op} }, \mathbf {Set} }$ be the contravariant functor category.
Then the Yoneda embedding $h_- : {\mathbf C} \to \sqbrk { {\mathbf C}^{\operatorname {op} }, \mathbf {Set} }$ is a fully faithful embedding.

Proof:
Let $X, Y \in \mathbf C$ be objects.
Then $\map {\operatorname {Hom} _{\mathbf C} } {X, Y}$ is a set, since $\mathbf C$ is locally small.
We need to show that $f \mapsto h_f$ induces a bjection:
:$\map {\operatorname {Hom} _{\mathbf C} } {X, Y} \to \map {\operatorname {Hom} _{\sqbrk { {\mathbf C}^{\operatorname {op} }, \mathbf {Set} } } } {h_X, h_Y}$
{{proof wanted|use Yoneda Lemma for Contravariant Functors}}
Category:Category Theory
82wqawmvspq5422kwfq176ma9arpt98
Theorem: Bijection in Yoneda Lemma for Covariant Functors

Let $F: \mathbf C \to \mathbf {Set}$ be a covariant functor.
Let $A \in \mathbf C$ be an object.
Let $\operatorname{id}_A$ be its identity morphism.
Let $h^A = \map {\operatorname {Hom} } {A, -}$ be its covariant hom-functor.
The class of natural transformations $\map {\operatorname {Nat} } {h^A, F}$ is a small class, and:
:$\alpha: \map {\operatorname {Nat} } {h^A, F} \to \map F A: \eta \mapsto \map {\eta_A} {\operatorname{id}_A}$
:$\beta: \map F A \to \map {\operatorname {Nat} } {h^A, F}: u \mapsto \paren {X \mapsto \paren {f \mapsto \map {\paren {\map F f} } u} }$
are inverses of each other.

Proof:
The fact that $\map {\operatorname {Nat} } {h^A, F}$ is a small class follows when we prove that the mappings are bijections.
Theorem: Naturality of Yoneda Lemma for Contravariant Functors

Let $[{\mathbf C}^{\operatorname{op}}, \mathbf{Set}]$ be the contravariant functor category.
Let ${\mathbf C}^{\operatorname{op}} \times [{\mathbf C}^{\operatorname{op}}, \mathbf{Set}] $ be the product category.
Let ${\mathbf C}^{\operatorname{op}} \times [{\mathbf C}^{\operatorname{op}}, \mathbf{Set}] \to \mathbf{Set} : (A, F) \mapsto \operatorname{Nat}(h_A, F)$ be the covariant functor defined as the composition of the hom bifunctor and the product of the opposite of the covariant Yoneda functor $h_-$ and the identity functor $\operatorname{id}_{[{\mathbf C}^{\operatorname{op}}, \mathbf{Set}]}$.
Let $\operatorname{ev} : {\mathbf C}^{\operatorname{op}} \times [{\mathbf C}^{\operatorname{op}}, \mathbf{Set}] \to \mathbf{Set} : (A, F) \mapsto F(A)$ be the contravariant functor evaluation functor.
Then $\Phi_{(A, F)} : \operatorname{Nat}(h_A, F) \to F(A) : \eta \mapsto \eta_A(\operatorname{id}_A)$ defines a natural isomorphism, where $\operatorname{id}_A$ is the identity morphism of $A$.

Proof:
{{proof wanted|from Naturality of Yoneda Lemma for Covariant Functors, by duality}}
Theorem: Period of Reciprocal of Repunit 1031 is 1031

The decimal expansion of the reciprocal of the repunit prime $R_{1031}$ has a period of $1031$.
:$\dfrac 1 {R_{1031}} = 0 \cdotp \underbrace{\dot 000 \ldots 000}_{1030} \dot 9$
{{refactor|Extract the fact that this is a unique period prime into another page}}
This is the only prime number to have a period of exactly $1031$.

Proof:
The reciprocal of a repunit $R_n$ is of the form:
:$\dfrac 1 {R_n} = 0 \cdotp \underbrace{\dot 000 \ldots 000}_{n - 1} \dot 9$
Thus $\dfrac 1 {R_{1031}}$ has a period of $1031$.
From Period of Reciprocal of Prime, for prime numbers such that:
:$p \nmid 10$
we have that the period of such a prime is the order of $10$ modulo $p$.
That is, the smallest integer $d$ such that:
:$10^d \equiv 1 \pmod p$
The only other possible primes $p$ whose reciprocals might have a period of $1031$ must also satisfy:
:$10^{1031} \equiv 1 \pmod p$
that is:
:$p \divides \paren {10^{1031} - 1} = 9 \times R_{1031}$
Therefore the only other possible prime whose reciprocal might have a period of $1031$ is $3$.
Trivially:
:$\dfrac 1 3 = 0 \cdotp \dot 3$
which has a period of $1$.
Hence the result.
{{qed}}
Theorem: Titanic Prime whose Digits are all Prime

The integer defined as:
:$7352 \times \dfrac {10^{1104} - 1} {10^4 - 1} + 1$
is a titanic prime all of whose digits are themselves prime.
That is:
:$\underbrace{7352}_{275} 7353$

Proof:
It is clear that the digits are instances of $7$, $3$, $5$ and $2$, and so are all prime.
It is also noted that it has $275 \times 4 + 4 = 1104$ digits, making it titanic.
{{Alpertron-factorizer|date = $6$th March $2022$|time = $2.1$ seconds}}
Theorem: Titanic Prime whose Digits are all 0 or 1

The integer defined as:
:$10^{641} \times \dfrac {10^{640} - 1} 9 + 1$
is a titanic prime all of whose digits are either $0$ or $1$.
That is:
:$\paren 1_{640} \paren 0_{640} 1$
where $\paren a_b$ means $b$ instances of $a$ in a string.

Proof:
It is clear that the digits are instances of $0$ and $1$.
It is also noted that it has $640 \times 2 + 1 = 1281$ digits, making it titanic.
{{Alpertron-factorizer|date = $6$th March $2022$|time = $2.5$ seconds}}
Theorem: Titanic Prime whose Digits are all 9 except for one 1

The integer defined as:
:$2 \times 10^{3020} - 1$
is a titanic prime all of whose digits are $9$ except one, which is $1$.
That is:
:$1 \left({9}\right)_{3020}$
where $\left({a}\right)_b$ means $b$ instances of $a$ in a string.

Proof:
It is clear that the digits are instances of $9$ except for the first $1$.
It is also noted that it has $3020 + 1 = 3021$ digits, making it titanic.
{{Alpertron-factorizer|date = $6$th March $2022$|time = $25.8$ seconds}}
Theorem: Titanic Prime consisting of 111 Blocks of each Digit plus Zeroes

The integer defined as:
:$\paren {123456789}_{111} \paren 0_{2284} 1$
where $\paren a_b$ means $b$ instances of $a$ in a string, is a titanic prime.

Proof:
It is noted that it has $9 \times 111 + 2284 + 1 = 3284$ digits, making it titanic.
It can be expressed arithmetically as:
:$123456789 \times \dfrac {10^{999} - 1} {10^9 - 1} \times 10^{2285} + 1$
{{Alpertron-factorizer|date = $6$th March $2022$|time = $50.2$ seconds}}
Theorem: Titanic Prime whose Digits are all Odd

The integer defined as:
:$1358 \times 10^{3821} - 1$
is a titanic prime all of whose digits are odd.
That is:
:$1357 \paren 9_{3821}$
where $\paren a_b$ means $b$ instances of $a$ in a string.

Proof:
It is clear that the digits are all instances of $9$ except for the initial $1357$, all of which are odd.
It is also noted that it has $4 + 3821 = 3825$ digits, making it titanic.
{{Alpertron-factorizer|date = $6$th March $2022$|time = $34.4$ seconds}}
Theorem: Pair of Titanic Twin Primes

The integers defined as:
:$190 \, 116 \times 3003 \times 10^{5120} \pm 1$
are a pair of titanic twin primes.
That is:
:$570 \, 918 \, 347 \paren 9_{5820}$
and:
:$570 \, 918 \, 348 \paren 0_{5819} 1$
where $\paren a_b$ means $b$ instances of $a$ in a string.

Proof:
It is noted that these integers have $9 + 5820 = 5829$ digits, making them titanic.
{{Alpertron-factorizer|date = $6$th March $2022$|time = $45$ seconds}}
Theorem: Gigantic Palindromic Prime

The integer defined as:
:$10^{11 \, 810} + 1 \, 465 \, 641 \times 10^{5902} + 1$
is a gigantic prime which is also palindromic.
That is:
:$1(0)_{5901}1465641(0)_{5901}1$
where $\left({a}\right)_b$ means $b$ instances of $a$ in a string.

Proof:
It is clear that this number is palindromic.
It is also noted that it has $1 + 5901 + 7 + 5901 + 1 = 11 \, 811$ digits, making it gigantic.
{{Alpertron-factorizer|date = $6$th March $2022$|time = $4$ minutes}}
Theorem: Zeroth Hyperoperation is Successor Function

The '''zeroth hyperoperation''' is the successor function:
:$H_0 \left({x, y}\right) = y + 1$

Proof:
Immediate by definition of the successor function $s: \Z_{\ge 0} \to  \Z_{\ge 0}$:
:$\forall y \in \Z_{\ge 0}: s \left({y}\right) = y + 1$
and for the $n$th hyperoperation:
$\forall n, x, y \in \Z_{\ge 0}: H_n \left({x, y}\right) = \begin{cases}
y + 1 & : n = 0 \\
x & : n = 1, y = 0 \\
0 & : n = 2, y = 0 \\
1 & : n > 2, y = 0 \\
H_{n - 1} \left({x, H_n \left({x, y - 1}\right)}\right) & : n > 0, y > 0 \end{cases}$
setting $n = 0$.
Thus the zeroth hyperoperation degenerates to a mapping with a single operand.
{{qed}}
Category:Hyperoperation
sva9ij9r42p3rhawixy5b3t0l4cgaw6
Theorem: First Hyperoperation is Addition Operation

The '''$1$st hyperoperation''' is the addition operation restricted to the positive integers:
:$\forall x, y \in \Z_{\ge 0}: H_1 \left({x, y}\right) = x + y$

Proof:
By definition of the hyperoperation sequence:
:$\forall n, x, y \in \Z_{\ge 0}: H_n \left({x, y}\right) = \begin{cases}
y + 1 & : n = 0 \\
x & : n = 1, y = 0 \\
0 & : n = 2, y = 0 \\
1 & : n > 2, y = 0 \\
H_{n - 1} \left({x, H_n \left({x, y - 1}\right)}\right) & : n > 0, y > 0 \end{cases}$
Thus the $1$st hyperoperation is defined as:
:$\forall x, y \in \Z_{\ge 0}: H_1 \left({x, y}\right) = \begin{cases}
x & : y = 0 \\
H_0 \left({x, H_1 \left({x, y - 1}\right)}\right) & : y > 0 \end{cases}$
From Zeroth Hyperoperation is Successor Function:
:$(1): \quad \forall x, y \in \Z_{\ge 0}: H_1 \left({x, y}\right) = \begin{cases}
x & : y = 0 \\
H_1 \left({x, y - 1}\right) + 1 & : y > 0 \end{cases}$
The proof proceeds by induction.
For all $y \in \Z_{\ge 0}$, let $P \left({y}\right)$ be the proposition:
:$\forall x \in \Z_{\ge 0}: H_1 \left({x, y}\right) = x + y$
Theorem: Second Hyperoperation is Multiplication Operation

The '''$2$nd hyperoperation''' is the multiplication operation restricted to the positive integers:
:$\forall x, y \in \Z_{\ge 0}: H_2 \left({x, y}\right) = x \times y$

Proof:
By definition of the hyperoperation sequence:
:$\forall n, x, y \in \Z_{\ge 0}: H_n \left({x, y}\right) = \begin{cases}
y + 1 & : n = 0 \\
x & : n = 1, y = 0 \\
0 & : n = 2, y = 0 \\
1 & : n > 2, y = 0 \\
H_{n - 1} \left({x, H_n \left({x, y - 1}\right)}\right) & : n > 0, y > 0 \end{cases}$
Thus the $2$nd hyperoperation is defined as:
:$\forall x, y \in \Z_{\ge 0}: H_2 \left({x, y}\right) = \begin{cases}
0 & : y = 0 \\
H_1 \left({x, H_2 \left({x, y - 1}\right)}\right) & : y > 0 \end{cases}$
From First Hyperoperation is Addition Operation:
:$(1): \quad \forall x, y \in \Z_{\ge 0}: H_2 \left({x, y}\right) = \begin{cases}
0 & : y = 0 \\
x + H_2 \left({x, y - 1}\right) & : y > 0 \end{cases}$
The proof proceeds by induction.
For all $y \in \Z_{\ge 0}$, let $P \left({y}\right)$ be the proposition:
:$\forall x \in \Z_{\ge 0}: H_2 \left({x, y}\right) = x \times y$
Theorem: Third Hyperoperation is Integer Power Operation

The '''$3$rd hyperoperation''' is the integer power operation restricted to the positive integers:
:$\forall x, y \in \Z_{\ge 0}: H_3 \left({x, y}\right) = x^y$

Proof:
By definition of the hyperoperation sequence:
:$\forall n, x, y \in \Z_{\ge 0}: H_n \left({x, y}\right) = \begin{cases}
y + 1 & : n = 0 \\
x & : n = 1, y = 0 \\
0 & : n = 2, y = 0 \\
1 & : n > 2, y = 0 \\
H_{n - 1} \left({x, H_n \left({x, y - 1}\right)}\right) & : n > 0, y > 0 \end{cases}$
Thus the $3$rd hyperoperation is defined as:
:$\forall x, y \in \Z_{\ge 0}: H_3 \left({x, y}\right) = \begin{cases}
1 & : y = 0 \\
H_2 \left({x, H_3 \left({x, y - 1}\right)}\right) & : y > 0 \end{cases}$
From Second Hyperoperation is Multiplication Operation:
:$(1): \quad \forall x, y \in \Z_{\ge 0}: H_3 \left({x, y}\right) = \begin{cases}
1 & : y = 0 \\
x \times H_3 \left({x, y - 1}\right) & : y > 0 \end{cases}$
The proof proceeds by induction.
For all $y \in \Z_{\ge 0}$, let $P \left({y}\right)$ be the proposition:
:$\forall x \in \Z_{\ge 0}: H_3 \left({x, y}\right) = x^y$
Theorem: Fourth Hyperoperation is Tetration Operation

The '''$4$th hyperoperation''' is the tetration operation restricted to the positive integers:
:$\forall x, y \in \Z_{\ge 0}: H_4 \left({x, y}\right) = x \uparrow \uparrow y$
where $\uparrow \uparrow$ denotes tetration:
:$x \uparrow \uparrow n := \begin{cases}
1 & : n = 0 \\
x \uparrow \left({x \uparrow \uparrow \left({n - 1}\right)}\right) & : n > 0 \\
\end{cases}$
In this context, $x \uparrow y$ is the Knuth notation for powers:
:$x \uparrow y := x^y$

Proof:
By definition of the hyperoperation sequence:
:$\forall n, x, y \in \Z_{\ge 0}: H_n \left({x, y}\right) = \begin{cases}
y + 1 & : n = 0 \\
x & : n = 1, y = 0 \\
0 & : n = 2, y = 0 \\
1 & : n > 2, y = 0 \\
H_{n - 1} \left({x, H_n \left({x, y - 1}\right)}\right) & : n > 0, y > 0 \end{cases}$
Thus the $4$th hyperoperation is defined as:
:$\forall x, y \in \Z_{\ge 0}: H_4 \left({x, y}\right) = \begin{cases}
1 & : y = 0 \\
H_3 \left({x, H_4 \left({x, y - 1}\right)}\right) & : y > 0 \end{cases}$
From Third Hyperoperation is Integer Power Operation:
:$(1): \quad \forall x, y \in \Z_{\ge 0}: H_4 \left({x, y}\right) = \begin{cases}
1 & : y = 0 \\
x \uparrow H_3 \left({x, y - 1}\right) & : y > 0 \end{cases}$
The proof proceeds by induction.
For all $y \in \Z_{\ge 0}$, let $P \left({y}\right)$ be the proposition:
:$\forall x \in \Z_{\ge 0}: H_4 \left({x, y}\right) = x \uparrow \uparrow y$
Theorem: Largest Integer Expressible by 3 Digits/Logarithm Base 10

:$\map {\log_{10} } {9^{9^9} } \approx 369 \, 693 \,099 \cdotp 63157 \, 03685 \, 87876 \, 1$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\log_{10} } {9^{9^9} }
      | r = 9^9 \times \log_{10} 9
      | c = 
}}
{{eqn | o = \approx
      | r = 387 \, 420 \, 489 \times 0\cdotp 95424 \, 25094 \, 393249
      | c = by calculator
}}
{{eqn | o = \approx
      | r = 369 \, 693 \, 099 \cdotp 63157 \, 03685 \, 87876 \, 1
      | c = by calculator
}}
{{end-eqn}}
{{qed}}