avewright/proofwiki-math huggingface dataset:
Theorem: Subgroup of Real Numbers is Discrete or Dense

Let $G$ be a subgroup of the additive group of real numbers.
Then one of the following holds:
:$G$ is dense in $\R$.
:$G$ is discrete and there exists $a \in \R$ such that $G = a \Z$, that is, $G$ is cyclic.

Proof:
If $G$ is trivial, then $G$ is discrete and cyclic.
Let $G$ be non-trivial.
Because $x \in G \iff -x \in G$, $G$ has a strictly positive element.
Thus $G \cap \R_{>0}$ is non-empty.
We have that $G \cap \R_{>0}$ is bounded below by $0$.
Hence, by the Continuum Property, $G \cap \R_{>0}$ admits an infimum.
So, let $a = \map \inf {G \cap \R_{>0} }$.
Theorem: Discrete Subgroup of Real Numbers is Closed

Let $G$ be a subgroup of the additive group of real numbers.
Let $G$ be discrete.
Then $G$ is closed.

Proof:
By Subgroup of Real Numbers is Discrete or Dense, there exists $a \in \R$ such that $G = a \Z$.
If $a = 0$, then $G$ is closed.
Let $a > 0$.
Then:
:$\ds \R \setminus G = \bigcup_{z \mathop \in \Z} \openint {a z} {a z + a}$
{{explain|Why?}}
By Union of Open Sets of Metric Space is Open, $\R\setminus G$ is open.
Thus $G$ is closed.
{{qed}}
Theorem: Conditions for Function to be First Integral of Euler's Equations for Vanishing Variation

Let $\Phi = \map {\Phi} {x, \family {y_i}_{1 \mathop \le i \mathop \le n}, \family {p_i}_{1 \mathop \le i \mathop \le n} }$ be a real function.
Let $H$ be Hamiltonian.
Then a necessary and sufficient condition for $\Phi$ to be the first integral of Euler's Equations is
:$\dfrac {\partial \Phi} {\partial x} + \sqbrk{\Phi, H} = 0$

Proof:
{{begin-eqn}}
{{eqn | l = \dfrac {\d \Phi} {\d x}
      | r = \frac {\partial\Phi} {\partial x} + \sum_{i \mathop = 1}^n \frac {\partial \Phi} {\partial y_i} \frac {\partial y_i} {\partial x} + \sum_{i \mathop = 1}^n \frac {\partial \Phi} {\partial p_i} \frac{\partial p_i} {\partial x}
}}
{{eqn | r = \frac {\partial \Phi} {\partial x} + \sum_{i \mathop = 1}^n \frac {\partial \Phi} {\partial y_i} \frac {\partial H} {\partial p_i} - \sum_{i \mathop = 1}^n \frac {\partial \Phi} {\partial p_i} \frac{\partial H} {\partial y_i}
}}
{{eqn | r = \frac {\partial \Phi} {\partial x} + \sqbrk{\Phi, H}
}}
{{end-eqn}}
For $\Phi$ to be the first integral:
:$\dfrac {\d \Phi} {\d x} = 0$
Hence the result.
{{qed}}
{{finish|get proof for the other condition}}
Theorem: Coarser Between Generator Set and Filter is Generator Set of Filter

Let $L = \struct {S, \wedge, \preceq}$ be a meet semilattice.
Let $F$ be a filter on $L$.
Let $G$ be a generator set of $F$.
Let $A$ be a subset of $S$ such that
:$G$ is coarser than $A$ and $A$ is coarser than $F$.
Then $A$ is generator set of $F$.

Proof:
By definition of generator set of filter:
:$F = \paren {\map {\operatorname {fininfs} } G}^\succeq$
where
:$\map {\operatorname {fininfs} } G$ denotes the finite infima set of $G$,
:$A^\succeq$ denotes the upper closure of $A$.
By Finite Infima Set of Coarser Subset is Coarser than Finite Infima Set:
:$\map {\operatorname {fininfs} } G$ is coarser than $\map {\operatorname {fininfs} } A$
Thus by Upper Closure of Coarser Subset is Subset of Upper Closure:
:$F \subseteq \paren {\map {\operatorname {fininfs} } A}^\succeq$
By filter in ordered set:
:$F$ is an upper section.
By Set Coarser than Upper Section is Subset:
:$A \subseteq F$
Thus by Finite Infima Set and Upper Closure is Smallest Filter:
:$\paren {\map {\operatorname {fininfs} } A}^\succeq \subseteq F$
Thus by definition of set equality:
:$F = \paren {\map {\operatorname {fininfs} } A}^\succeq$
Hence $A$ is generator set of $F$.
{{qed}}
Theorem: Borsuk-Ulam Theorem

Let $n$ be a positive integer.
Let $f: \mathbb S^n \to \R^n$ be a continuous mapping from an $n$-sphere to $\R^n$.
Then there exists $x \in \mathbb S^n$ such that $\map f x = \map f {-x}$.

Proof:
{{ProofWanted}}
{{Namedfor|Karol Borsuk|name2 = Stanisław Marcin Ulam|cat = Borsuk|cat2 = Ulam}}
Category:Algebraic Topology
i7z9kevixtqhdfvgow1fbiagjqjis94
Theorem: Gershgorin Circle Theorem

Let $n$ be a positive integer.
Let $A = \sqbrk {a_{i j} }$ be a complex square matrix of order $n$.
Let $\lambda$ be an eigenvalue of $A$.
Then there exists $i \in \set {1, 2, \ldots, n}$ such that:
:$\lambda \in \map {\mathbb D} {a_{i i}, R_i}$
where:
:$\ds R_i = \sum_{j \mathop \ne i} \cmod {a_{ i j} }$
:$\map {\mathbb D} {a, R}$ denotes the complex disk of center $a$ and radius $R$.

Proof:
{{ProofWanted}}
{{Namedfor|Semyon Aranovich Gershgorin|cat = Gershgorin}}
Theorem: Homotopic Paths Implies Homotopic Composition

Let $T = \left({S, \tau}\right)$ be a topological space.
Let $f_1, f_2, g_1, g_2: \left[{0 \,.\,.\, 1}\right] \to S$ be paths in $T$.
Let $f_1$ be homotopic to $f_2$ and $g_1$ be homotopic to $g_2$.
Then the concatenated paths $f_1 * g_1$ and $f_2 * g_2$ are homotopic.

Proof:
Let $F: \left[{0 \,.\,.\, 1}\right] \times \left[{0 \,.\,.\, 1}\right] \to S$ be a homotopy between $f_1$ and $f_2$.
Let $G: \left[{0 \,.\,.\, 1}\right] \times \left[{0 \,.\,.\, 1}\right] \to S$ be a homotopy between $g_1$ and $g_2$.
Define $H: \left[{0 \,.\,.\, 1}\right] \times \left[{0 \,.\,.\, 1}\right] \to S$ by:
:$H \left({s, t}\right) = \begin{cases} F \left({2 s, t}\right) & : s \in \left[{0 \,.\,.\, \dfrac 1 2}\right] \\
G \left({2 s - 1, t}\right) & : s \in \left[{\dfrac 1 2 \,.\,.\, 1}\right]\end{cases}$
By Continuous Mapping on Finite Union of Closed Sets, $H$ is continuous.
By definition of concatenation of paths, $H$ is a homotopy between $f_1 * g_1$ and $f_2 * g_2$.
{{qed}}
Theorem: Finite Infima Set of Coarser Subset is Coarser than Finite Infima Set

Let $L = \struct {S, \wedge, \preceq}$ be a meet semilattice.
Let $A, B$ be subsets of $S$ such that
:$A$ is coarser than $B$.
Then $\map {\operatorname{fininfs} } A$ is coarser than $\map {\operatorname{fininfs} } B$
where $\map {\operatorname{fininfs} } B$ denotes the finite infima set of $B$.

Proof:
Let $x \in \map {\operatorname{fininfs} } A$
By definition of finite infima set:
:$\exists Y \in \map {\operatorname {Fin} } A: x = \inf Y$ and $Y$ admits an infimum,
where $\map {\operatorname {Fin} } A$ denotes the set of all finite subsets of $A$.
By definition of coarser subset:
:$\forall y \in Y: \exists z \in B: z \preceq y$
By Axiom of Choice:
:$\exists f: Y \to B: \forall y \in Y: \map f y \preceq y$
We will prove that
:$f \sqbrk Y$ admits an infimum.
In the case when $Y = \O$:
By Image of Empty Set is Empty Set: Corollary 1:
:$f \sqbrk Y = \O$
Thus
:$f \sqbrk Y$ admits an infimum.
In the case when $Y \ne \O$
By definition of non-empty set:
:$\exists y: y \in Y$
By definition of image of set:
:$\map f y \in f \sqbrk Y$
By Image of Mapping from Finite Set is Finite:
:$f \sqbrk Y$ is a finite set.
Thus by Existence of Non-Empty Finite Infima in Meet Semilattice:
:$f \sqbrk Y$ admits an infimum.
{{qed|lemma}}
We will prove that:
:$\inf f \sqbrk Y$ is lower bound for $Y$.
Let $y \in Y$.
By definition of $f$:
:$\map f y \preceq y$
By definition of image of set:
:$\map f y \in f \sqbrk Y$
By definitions of infimum and lower bound:
:$\inf f \sqbrk Y \preceq \map f y$
Thus by definition of transitivity:
:$\inf f \sqbrk Y \preceq y$
{{qed|lemma}}
By definition of infimum:
:$\inf f \sqbrk Y \preceq x$
By definition of finite infima set:
:$\inf f \sqbrk Y \in \map {\operatorname{fininfs} } B$
Thus
:$\exists y \in \map {\operatorname{fininfs} } B: y \preceq x$
{{qed}}
Theorem: Legendre Transform is Involution

The Legendre transform is an Involution.

Proof:
Let $\map f x$ be a strictly convex real function.
Let $p = \map {f'} x$.
By definition of the Legendre transform, the transformed real function is of the form:
:$\map {f^*} p = - \map f {\map x p} + p \map x p$
By Legendre Transform of Strictly Convex Real Function is Strictly Convex, $f^*$ is strictly convex.
Let $t = \map { {f^*}'} p$.
Let $\map {\paren {f^*}^*} t = - \map {f^*} {\map p t} + t \map p t$.
Then:
{{begin-eqn}}
{{eqn | l = \paren {f^*}^*
      | r = -f^* + t p 
}}
{{eqn | r = -\paren {-f + p t} + t p 
}}
{{eqn | r = f
}}
{{end-eqn}}
$t$ is an arbitrary independent variable, hence can be renamed.
Set $t = x$.
Then:
:$\tuple {t,f^{**} } = \tuple {x, f}$
which is the original pair of function and its variable.
Hence, by definition, the Legendre transform is an involution.
{{qed}}
Theorem: Upper Closure of Coarser Subset is Subset of Upper Closure

Let $L = \left({S, \preceq}\right)$ be a preordered set.
Let $A, B$ be subsets of $S$ such that
:$A$ is coarser than $B$.
Then $A^\succeq \subseteq B^\succeq$

Proof:
Let $x \in A^\succeq$
By definition of upper closure of subset:
:$\exists y \in A: y \preceq x$
By definition of coarser subset:
:$\exists z \in B: z \preceq y$
By definition of transitivity:
:$z \preceq x$
Thus by definition of upper closure of subset:
:$x \in B^\succeq$
{{qed}}
Theorem: Set Coarser than Upper Section is Subset

Let $\struct {S, \preceq}$ be a preordered set.
Let $A, B$ be subsets of $S$ such that
:$A$ is coarser than $B$
and
:$B$ is an upper section.
Then:
:$A \subseteq B$

Proof:
Let $x \in A$.
By definition of coarser subset:
:$\exists y \in B: y \preceq x$
Thus by definition of upper section:
:$x \in B$
{{qed}}
Theorem: Sum of 4 Unit Fractions that equals 1

There are $14$ ways to represent $1$ as the sum of exactly $4$ unit fractions.

Proof:
Let:
:$1 = \dfrac 1 a + \dfrac 1 b + \dfrac 1 c + \dfrac 1 d$
where:
:$a \le b \le c \le d$
and:
:$a \ge 2$
Theorem: Conditions for Function to be Maximum of its Legendre Transform Two-variable Equivalent

Let $x, p \in \R$.
Let $\map f x$ be a strictly convex real function.
Let $f^*$ be a Legendre transformed $f$.
Let $\map g {x, p} = - \map {f^*} p + x p$
Then:
:$\ds \map f x = \max_p \paren {-\map {f^*} p + x p}$
where $\ds \max_p$ maximises the function with respect to a variable $p$.

Proof:
Function $g$ acquires an extremum along $p$, when its first derivative along $p$ vanishes:
{{begin-eqn}}
{{eqn | l = \frac {\partial g} {\partial p}  
      | r = -\frac {\partial f^*} {\partial p} + x
}}
{{eqn | r = 0
      | c = Extremum condition
}}
{{eqn | ll= \leadsto
      | l = \map { {f^*}'} p
      | r = x
}}
{{end-eqn}}
To check if the extremum is a global maximum, consider the second derivative:
:$\dfrac {\partial^2 g} {\partial p^2} = - \dfrac {\partial^2 f^*} {\partial p^2}$
By Legendre Transform of Strictly Convex Real Function is Strictly Convex and Real Function is Strictly Convex iff Derivative is Strictly Increasing, it holds that:
{{begin-eqn}}
{{eqn | l = \frac {\partial^2 f^*} {\partial p^2}
      | o = >
      | r = 0
}}
{{eqn | ll= \leadsto
      | l = \frac {\partial^2 g} {\partial p^2}
      | o = <
      | r = 0
}}
{{eqn | ll= \leadsto
      | l = \valueat {\frac {\partial^2 g} {\partial p^2} } {\frac {\partial g} {\partial p} \mathop = 0}
      | o = <
      | r = 0
}}
{{end-eqn}}
Negative second derivative at the extremum implies extremum being a global maximum.
Therefore:
:$\ds \max_p \paren{-\map {f^*} p + x p} = \bigvalueat {\paren {-\map {f^*} p + x p} } {x \mathop = \map { {f^*}'} p}$
The {{RHS}} is the Legendre Transform of $f^*$.
However, $f^*$ is a Legendre transformed $f$.
By Legendre Transform is Involution, this equals $f$.
{{qed}}
{{Finish|clean up local/global extrema ambiguity}}
Theorem: Set is Coarser than Image of Mapping of Infima

Let $\struct {S, \wedge, \preceq}$ be a meet semilattice.
Let $f, g:\N \to S$ be mappings such that:
:$\forall n \in \N: \map g n = \inf \set {\map f m: m \in \N \land m \le n}$
Then $f \sqbrk \N$ is coarser than $g \sqbrk \N$
where $f \sqbrk \N$ denotes the image of mapping $f$.

Proof:
Let $x \in f \sqbrk \N$.
By definition of image of mapping:
:$\exists n \in \N: x = \map f n$
By definition of $g$:
:$\map g n = \inf \set {\map f m: m \in \N \land m \le n}$
By definition of reflexivity:
:$n \le n$
Then
:$\map f n \in \set {\map f m: m \in \N \land m \le n}$
By definitions of infimum and lower bound:
:$\map g n \preceq x$
By definition of image of mapping:
:$\map g n \in g \sqbrk \N$
Thus
:$\exists y \in g \sqbrk \N: y \preceq x$
{{qed}}
Theorem: Solutions of Ramanujan-Nagell Equation

Integer solutions to the Ramanujan-Nagell equation:
:$x^2 + 7 = 2^n$
exist for only $5$ values of $n$:
:$3, 4, 5, 7, 15$
{{OEIS|A060728}}
The corresponding values of $x$ are:
:$1, 3, 5, 11, 181$
{{OEIS|A038198}}

Proof:
By direct implementation:
{{begin-eqn}}
{{eqn | n = 1
      | l = 1^2 + 7
      | r = 1 + 7
      | c = 
}}
{{eqn | r = 8
      | c = 
}}
{{eqn | r = 2^3
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | n = 2
      | l = 3^2 + 7
      | r = 9 + 7
      | c = 
}}
{{eqn | r = 16
      | c = 
}}
{{eqn | r = 2^4
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | n = 3
      | l = 5^2 + 7
      | r = 25 + 7
      | c = 
}}
{{eqn | r = 32
      | c = 
}}
{{eqn | r = 2^5
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | n = 4
      | l = 11^2 + 7
      | r = 121 + 7
      | c = 
}}
{{eqn | r = 128
      | c = 
}}
{{eqn | r = 2^7
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | n = 5
      | l = 181^2 + 7
      | r = 32 \, 761 + 7
      | c = 
}}
{{eqn | r = 32 \, 768
      | c = 
}}
{{eqn | r = 2^{15}
      | c = 
}}
{{end-eqn}}
{{ProofWanted|It remains to be proved that these are the only solutions.}}
Theorem: Five Ramanujan-Nagell Numbers

There exist exactly $5$ Ramanujan-Nagell numbers: positive integers of the form $2^m - 1$ which are triangular:
:$0, 1, 3, 15, 4095$
{{OEIS|A076046}}

Proof:
Consider the numbers of the form $2^m - 1$ which are triangular:
{{begin-eqn}}
{{eqn | l = 2^m - 1
      | r = \frac {r \paren {r + 1} } 2
      | c = Closed Form for Triangular Numbers
}}
{{eqn | ll= \leadstoandfrom
      | l = 8 \paren {2^m - 1}
      | r = 4 r \paren {r + 1}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = 2^{m + 3} - 8
      | r = 4 r^2 + 4 r
      | c = 
}}
{{eqn | n = 1
      | ll= \leadstoandfrom
      | l = 2^{m + 3} - 7
      | r = 4 r^2 + 4 r + 1
      | c = 
}}
{{eqn | r = \paren {2 r + 1}^2
      | c = 
}}
{{end-eqn}}
Let:
:$n = m - 3$
:$x = 2 r + 1$
and it can be seen that $(1)$ is equivalent to:
:$x^2 + 7 = 2^n$
From Solutions of Ramanujan-Nagell Equation:
:$x = 1, 3, 5, 11, 181$
Setting $r = \dfrac {x - 1} 2$ it is seen that the corresponding triangular numbers are:
:$\dfrac {\paren {x - 1} \paren {x + 1} } 8$
Thus the corresponding Ramanujan-Nagell numbers are:
:$0, 1, 3, 15, 4095$
{{qed}}
Category:Ramanujan-Nagell Equation
Category:5
9b2wvfkp0b4yh5kp6hrj7pd90b6v5n6
Theorem: Conditions for Functional to be Extremum of Two-variable Functional over Canonical Variable p

Let $y = \map y x$ and $\map F {x, y, y'}$ be real functions.
Let $\dfrac {\partial^2 F} {\partial {y'}^2} \ne 0$.
Let $\ds J \sqbrk y = \int_a^b \map F {x, y, y'} \rd x$
Let $\ds J \sqbrk {y, p} = \int_a^b \paren {-\map H {x, y, p} + p y'} \rd x$, where $H$ is the Hamiltonian of $J \sqbrk y$.
Then $\ds J \sqbrk y = \bigvalueat {J \sqbrk {y, p} } {\frac {\delta J \sqbrk{y, p} } {\delta p} \mathop = 0}$

Proof:
Euler's equation for $J \sqbrk {y, p}$:
{{begin-eqn}}
{{eqn | l = \frac {\delta J \sqbrk{y, p} } {\delta p}
      | r = \frac {\partial} {\partial p} \paren {-\map H {x, y, p} + p y'}
      | c = Depends only on $p$ and not its derivatives
}}
{{eqn | r = -\frac {\partial H} {\partial p} + y'
}}
{{eqn | r = 0
}}
{{eqn | ll= \leadsto
      | l = y'
      | r = \frac {\partial H} {\partial p}
}}
{{end-eqn}}
Substitute this result back into the functional $J \sqbrk {y, p}$:
{{begin-eqn}}
{{eqn | l = \bigvalueat {J \sqbrk {y, p} } {\frac {\delta J \sqbrk {y, p} } {\delta p} \mathop = 0}
      | r = \int_a^b \paren {-H + p \frac{\partial H}{\partial p} } \rd x
}}
{{eqn | r = \int_a^b \paren {\map F {x, y, y'} - p y' + p \frac {\partial \paren {-\map F {x, y, y'} + p y'} } {\partial p} } \rd x
      | c = {{Defof|Hamiltonian}}
}}
{{eqn | r = \int_a^b \paren {\map F {x, y, y'} - p y' + p y'} \rd x
}}
{{eqn | r = \int_a^b \map F {x, y, y'} \rd x
}}
{{end-eqn}}
{{qed}}
Theorem: Image of Mapping of Infima is Generator Set of Filter

Let $\struct {S, \wedge, \preceq}$ be a meet semilattice.
Let $f, g:\N \to S$ be mappings such that:
:$\forall n \in \N: \map g n = \inf \set {\map f m: m \in \N \land m \le n}$
Let $F$ be a filter such that
:$f \sqbrk \N$ is generator set of $F$,
where $f \sqbrk \N$ denotes the image of $f$.
Then $g \sqbrk \N$ is generator set of $F$.

Proof:
By Set is Coarser than Image of Mapping of Infima:
:$f \sqbrk \N$ is coarser than $g \sqbrk \N$.
By definition of generator set of filter:
:$F = \paren {\map {\operatorname{fininfs} } {f \sqbrk N} }^\succeq$
where
:$\map {\operatorname{fininfs} } {f \sqbrk \N}$ denotes the finite infima set of $f \sqbrk \N$,
:for subset $A$ of $S$: $A^\succeq$ denotes upper closure of $A$.
By Finite Infima Set and Upper Closure is Smallest Filter:
:$f \sqbrk \N \subseteq F$
We will prove that:
:$g \sqbrk \N \subseteq F$
Let $x \in g \sqbrk \N$.
By definition of image of mapping:
:$\exists n \in \N: x = \map g n$
By definition of $g$:
:$x = \inf \set {\map f m: m \in \N \land m \le n}$
By definition:
:$\set {\map f m: m \in \N \land m \le n}$ is a finite set.
By definition of subset:
:$\set {\map f m: m \in \N \land m \le n} \subseteq F$
By definition of reflexivity:
:$\map f n \in \set {\map f m: m \in \N \land m \le n}$
Thus by Filtered in Meet Semilattice with Finite Infima:
:$x \in F$
{{qed|lemma}}
By Subset of Set is Coarser than Set:
:$g \sqbrk \N$ is coarser than $F$.
Thus by Coarser Between Generator Set and Filter is Generator Set of Filter:
:$g \sqbrk \N$ is generator set of $F$.
{{qed}}
Theorem: Subset of Set is Coarser than Set

Let $\left({S, \preceq}\right)$ be a preordered set.
Let $A, B$ be subset of $S$ such that
:$A \subseteq B$
Then $A$ is coarser than $B$.

Proof:
Let $x \in A$.
By definition of subset:
:$x \in B$
By definition of reflexivity:
:$x \preceq x$
Thus
:$\exists y \in B: y \preceq x$
{{qed}}
Theorem: Existence of Product of Three Distinct Primes between n and 2n

Let $n \in \Z$ be an integer such that $n > 15$.
Then between $n$ and $2 n$ there exists at least one integer which is the product of $3$ distinct prime numbers.

Proof:
Let $16 \le n \le 29$.
Then:
:$n < 30 < 2 n$
and we have:
:$30 = 2 \times 3 \times 5$
which is a product of $3$ distinct primes.
Hence the result holds for $n$ in that range.
Let $n \ge 30$.
Then by the Division Theorem:
:$\exists q, r \in \N: n = 6 q + r$, $0 \le r < 6$, $q \ge 5$
By Bertrand-Chebyshev Theorem, there is a prime $p$ where $5 \le q < p < 2 q$.
Hence $p$ is not $2$ or $3$, and:
{{begin-eqn}}
{{eqn | l = n
      | o = <
      | r = 6 \paren {q + 1}
      | c = 
}}
{{eqn | o = \le
      | r = 2 \times 3 \times p
}}
{{eqn | o = \le
      | r = 12 q
}}
{{eqn | o = \le
      | r = 2 n
}}
{{end-eqn}}
This proves the result.
{{qed}}
Theorem: Second Column and Diagonal of Pascal's Triangle consist of Triangular Numbers

The $2$nd column and $2$nd diagonal of Pascal's triangle consists of the set of triangular numbers.

Proof:
Recall Pascal's triangle:
{{:Definition:Pascal's Triangle}}
By definition, the entry in row $n$ and column $m$ contains the binomial coefficient $\dbinom n m$.
Thus the $2$nd column contains all the elements of the form $\dbinom n 2$.
The $m$th diagonal consists of the elements in column $n - m$.
Thus the $m$th diagonal contains the binomial coefficients $\dbinom n {n - m}$.
By Symmetry Rule for Binomial Coefficients:
:$\dbinom n {n - m} = \dbinom n m$
Thus the $2$nd diagonal also contains the binomial coefficients $\dbinom n 2$.
By Binomial Coefficient with Two: Corollary, the triangular numbers are precisely those numbers of the form $\dbinom n 2$.
Hence the result.
{{qed}}
Theorem: Complement of Element is Irreducible implies Element is Meet Irreducible

Let $T = \struct {S, \tau}$ be a topological space.
Let $P = \struct {\tau, \preceq}$ be an ordered set
where $\mathord \preceq = \mathord \subseteq \cap \paren {\tau \times \tau}$
Let $A \in \tau$.
Then $\relcomp S A$ is irreducible implies
$A$ is meet irreducible in $P$
where $\relcomp S A$ denotes the relative complement of $A$ relative to $S$.

Proof:
Assume that
:$\relcomp S A$ is irreducible.
Let $x, y \in \tau$ such that
:$A = x \wedge y$
By definition of topological space:
:$x \cap y \in \tau$
By Meet in Inclusion Ordered Set:
:$x \wedge y = x \cap y$
By De Morgan's Laws: Complement of Intersection:
:$\relcomp S A = \relcomp S x \cup \relcomp S y$
By definition:
:$\relcomp S x$ and $\relcomp S y$ are closed.
By definition of irreducible:
:$\relcomp S A = \relcomp S x$ or $\relcomp S A = \relcomp S y$
Thus by Relative Complement of Relative Complement:
:$A = x$ or $A = y$
{{qed}}
Theorem: Pentagonal Number as Sum of Triangular Numbers

Let $P_n$ be the $n$th pentagonal number.
Then:
:$P_n = T_n + 2 T_{n - 1}$
where $T_n$ is the $n$th triangular number.

Proof:
{{begin-eqn}}
{{eqn | l = T_n + 2 T_{n - 1}
      | r = \frac {n \paren {n + 1} } 2 + 2 \frac {\paren {n - 1} n} 2
      | c = Closed Form for Triangular Numbers
}}
{{eqn | r = \frac {n^2 + n + 2 \paren {n^2 - n} } 2
      | c = 
}}
{{eqn | r = \frac {3 n^2 - n} 2
      | c = 
}}
{{eqn | r = \frac {3 n \paren {n - 1} } 2
      | c = 
}}
{{eqn | r = P_n
      | c = Closed Form for Pentagonal Numbers
}}
{{end-eqn}}
{{qed}}
Theorem: Product of Two Triangular Numbers to make Square

Let $T_n$ be a triangular number.
Then there is an infinite number of $m \in \Z_{>0}$ such that $T_n \times T_m$ is a square number.

Proof:
Since $n^2 < n \paren {n + 1} < \paren {n + 1}^2$, $n \paren {n + 1}$ cannot be a square number.
Thus there are infinitely many distinct integer solutions to Pell's equation:
:$x^2 - n \paren {n + 1} y^2 = 1$
and for each solution:
{{begin-eqn}}
{{eqn | l = T_n T_{x^2 - 1}
      | r = \frac {n \paren {n + 1} } 2 \times \frac {x^2 \paren {x^2 - 1} } 2
      | c = Closed Form for Triangular Numbers
}}
{{eqn | r = \frac {n \paren {n + 1} } 2 \times \frac {x^2 n \paren {n + 1} y^2 } 2
}}
{{eqn | r = \paren {\frac {x y n \paren {n + 1} } 2}^2
}}
{{end-eqn}}
Hence the result.
{{qed}}