avewright/proofwiki-math huggingface dataset:
Theorem: Order of Product of Entire Functions

Let $f, g: \C \to \C$ be entire functions of order $\alpha$ and $\beta$.
Then $f g$ has order at most $\map \max {\alpha, \beta}$.

Proof:
If $\map \max {\alpha, \beta} = +\infty$, the claim is trivial.
Thus we may assume that $\alpha < +\infty$ and $\beta < +\infty$.
Let $\epsilon > 0$ be arbitrary.
By {{Defof|Order of Entire Function|index=1}}, we have:
:$\map f z = \map \OO {\map \exp {\cmod z^{\alpha + \epsilon} } }$
and:
:$\map g z = \map \OO {\map \exp {\cmod z^{\beta + \epsilon} } }$
By {{Defof|Big-O Notation/Complex/Infinity}}, there are $c_1,c_2,r_1,r_2 \in \R$ such that:
:$\cmod z \ge r_1 \implies \cmod {\map f z} \le c_1 \map \exp {\cmod z^{\alpha + \epsilon} }$
and:
:$\cmod z \ge r_2 \implies \cmod {\map g z} \le c_2 \map \exp {\cmod z^{\beta + \epsilon} }$
Let $r_0 := \max \set {r_1, r_2, 2^{1 / \epsilon } }$.
Then, if $\cmod z \ge r_0$, we have:
{{begin-eqn}}
{{eqn | l = \cmod {\map f z \map g z}
      | o = \le
      | r = \paren { c_1 \map \exp {\cmod z^{\alpha + \epsilon} } } \paren {c_2 \map \exp {\cmod z^{\beta + \epsilon} } }
}}
{{eqn | r = c_1 c_2 \map \exp {\cmod z^{\alpha + \epsilon} + \cmod z^{\beta + \epsilon} }
}}
{{eqn | o = \le
      | r = c_1 c_2 \map \exp {2 \cmod z^{\map \max {\alpha, \beta}  + \epsilon} }
      | c = as $\cmod z \ge r_0 \ge 2^{1 / \epsilon} \ge 1$
}}
{{eqn | r = c_1 c_2 \map \exp {\paren {2 \cmod z^{-\epsilon} } \cmod z^{\map \max {\alpha, \beta}  + 2 \epsilon} }
}}
{{eqn | o = \le
      | r = c_1 c_2 \map \exp {\cmod z^{\map \max {\alpha, \beta}  + 2 \epsilon} }
      | c = as $\cmod z \ge 2^{1 / \epsilon}$
}}
{{end-eqn}}
Therefore the order of $fg$ is:
:$\le \map \max {\alpha, \beta} + 2 \epsilon$
Letting $\epsilon \to 0$, the claim follows.
{{qed}}
Theorem: Numbers Partitioned into up to 4 Squares in 5 Ways

The following positive integers can be expressed as the sum of no more than $4$ squares in $5$ distinct ways:
:$50, 52, 54, 58, \ldots$

Proof:
{{begin-eqn}}
{{eqn | l = 50
      | r = 7^2 + 1^2
      | c = 
}}
{{eqn | r = 5^2 + 5^2
      | c = 
}}
{{eqn | r = 5^2 + 4^2 + 3^2
      | c = 
}}
{{eqn | r = 4^2 + 4^2 + 3^2 + 3^2
      | c = 
}}
{{eqn | r = 6^2 + 3^2 + 2^2 + 1^2
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = 52
      | r = 7^2 + 1^2 + 1^2 + 1^2
      | c = 
}}
{{eqn | r = 6^2 + 4^2
      | c = 
}}
{{eqn | r = 5^2 + 5^2 + 1^2 + 1^2
      | c = 
}}
{{eqn | r = 4^2 + 4^2 + 4^2 + 2^2
      | c = 
}}
{{eqn | r = 5^2 + 3^2 + 3^2 + 3^2
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = 54
      | r = 7^2 + 2^2 + 1^2
      | c = 
}}
{{eqn | r = 6^2 + 4^2 + 1^2 + 1^2
      | c = 
}}
{{eqn | r = 6^2 + 3^2 + 3^2
      | c = 
}}
{{eqn | r = 5^2 + 5^2 + 2^2
      | c = 
}}
{{eqn | r = 5^2 + 4^2 + 3^2 + 2^2
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = 58
      | r = 7^2 + 3^2
      | c = 
}}
{{eqn | r = 7^2 + 2^2 + 2^2 + 1^2
      | c = 
}}
{{eqn | r = 6^2 + 3^2 + 3^2 + 2^2
      | c = 
}}
{{eqn | r = 5^2 + 5^2 + 2^2 + 2^2
      | c = 
}}
{{eqn | r = 5^2 + 4^2 + 4^2 + 1^2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Order of Product of Entire Function with Polynomial

Let $f: \C \to \C$ be an entire function of order $\omega$.
Let $P: \C \to \C$ be a nonzero polynomial.
Then $f \cdot P$ has order $\omega$.

Proof:
If $f=0$, then $f \cdot P = 0$.
Thus the claim is trivial.
Therefore suppose that $f$ is not identically zero.
By Order of Product of Entire Functions and Polynomial has Order Zero, $f\cdot P$ has order at most $\omega$.
By Limit at Infinity of Polynomial, there exist $r, \delta > 0$ such that $\size {\map P z} \ge \delta$ for $\size z \ge r$.
{{AimForCont}} $\ds \map \log {\max_{\size z \mathop \le R} \size {\map f z \map P z} } = \map \OO {R^\beta}$ for some $\beta < \omega$.
By the Maximum Modulus Principle:
:$\ds \max_{\size z \mathop \le R} \size {\map f z} \le \dfrac 1 \delta \max_{\size z \mathop \le R} \size {\map f z \map P z}$
for $R \ge r$.
Thus:
:$\ds \map \log {\max_{\size z \mathop \le R} \size {\map f z} } = \map \OO {R^\beta}$
By {{Defof|Order of Entire Function|index=2}}, this means:
:$\omega \le \beta$
This is a contradiction.
Thus $f \cdot P$ has order $\omega$.
{{qed}}
Theorem: Order of Shifted Entire Function

Let $f: \C \to \C$ be an entire function of order $\alpha$.
Let $a \in \C$.
Then $\map f {z + a}$ has order $\alpha$.

Proof:
We shall verify {{Defof|Order of Entire Function|index=3}}.
Let $\map g z := \map f {z + a}$ for $z \in \C$.
Then for all $R > \cmod a$:
:$\ds \max_{\cmod z \mathop \le R \mathop - \cmod a} \cmod {\map f z} \le \max_{\cmod z \mathop \le R} \cmod {\map g z} \le \max_{\cmod z \mathop \le R \mathop + \cmod a} \cmod {\map f z}$
Thus:
:$\paren 1 : \dfrac {\ds \ln \ln \max_{\cmod z \mathop \le R \mathop - \cmod a} \cmod {\map f z} }{\ln R} \le \dfrac {\ds \ln \ln \max_{\cmod z \mathop \le R} \cmod {\map g z} }{\ln R} \le \dfrac {\ds \ln \ln \max_{\cmod z \mathop \le R \mathop + \cmod a} \cmod {\map f z} }{\ln R}$
On the other hand, for each $c \in \R$:
:$\ds \paren 2 : \lim_{R \mathop \to +\infty} \dfrac {\map \ln {R + c} } {\ln R} = 1$
Thus:
{{begin-eqn}}
{{eqn | n = 3
      | o =
      | r = \limsup_{R \mathop \to +\infty} \dfrac {\ds \ln \ln \max_{\cmod z \mathop \le R \mathop - \cmod a} \cmod {\map f z} }{\ln R}
}}
{{eqn | r = \lim_{R \mathop \to +\infty} \dfrac {\map \ln {R - \cmod a} }{\ln R} \limsup_{R \mathop \to +\infty} \dfrac {\ds \ln \ln \max_{\cmod z \mathop \le R \mathop - \cmod a} \cmod {\map f z} }{\map \ln {R - \cmod a} }
      | c = Product Rule
}}
{{eqn | r = 1 \cdot \alpha
      | c = by $\paren 2$ and {{hypothesis}}
}}
{{eqn | r = \alpha
}}
{{end-eqn}}
Similarly, we have:
:$\ds \paren 4 : \limsup_{R \mathop \to +\infty} \dfrac {\ds \ln \ln \max_{\cmod z \mathop \le R + \cmod a} \cmod {\map f z} }{\ln R} = \alpha$
In view of $\paren 3$ and $\paren 4$, the claim follows from $\paren 1$ by Sandwich Rule.
{{qed}}
Theorem: Zerofree Entire Function of Finite Order is Exponential of Polynomial

Let $f: \C \to \C$ be an entire function of finite order.
Let $f$ have no zeroes.
Then $f = \exp P$ for some polynomial $P$.

Proof:
This is an immediate consequence of Hadamard Factorization Theorem.
{{qed}}
Category:Entire Functions
5u1070qxsmw80zn68uyesvu3g35yv5s
Theorem: Borel-Carathéodory Lemma

Let $D \subset \C$ be an open set with $0 \in D$.
Let $R > 0$ be such that the open disk $\map B {0, R} \subset D$.
Let $f: D \to \C$ be analytic with $\map f 0 = 0$.
Let $\map \Re {\map f z} \le M$ for $\cmod z \le R$.
Let $0 < r < R$.
Then for $\cmod z \le r$:
{{begin-eqn}}
{{eqn | n = 1
      | l = \cmod {\map f z}
      | o = \le
      | r = \frac {2 M r} {R - r}
}}
{{eqn | n = 2
      | q = \forall k \ge 1
      | l = \cmod {\map {f^{\paren k} } z}
      | o = \le
      | r = \frac {2 M R k!} {\paren {R - r}^{k + 1} }
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = \map f z
      | r = \sum_{n \mathop = 0}^\infty \frac {\map {f^{\paren n} } 0} {n!} z^n
      | c = Taylor Series of Holomorphic Function
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty \frac {\map {f^{\paren n} } 0} {n!} z^n
      | c = as $\map f 0 = 0$
}}
{{end-eqn}}
Theorem: Order of Sum of Entire Functions

Let $f, g: \C \to \C$ be entire functions of order $\alpha$ and $\beta$.
Then $f + g$ has order at most $\map \max {\alpha, \beta}$, with equality if $\alpha \ne \beta$.

Proof:
{{MissingLinks|Each step of this proof needs to be backed up with evidence: a link to a result or a definition, preferably.}}
Let $\map f z = \map \OO {e^{\cmod z^m} }$ and $\map g z = \map \OO {e^{\cmod z^k} }$.
{{WLOG}}, let $m \ge k$.
Then it follows that $\map f z + \map g z = \map \OO {e^{\cmod z^m} }$.
Then the order of $f + g$ is at most $m$.
Since $\alpha, \beta$ are the infima of $m, k$, it follows that the order of $f + g$ is at most $\alpha$.
Let $\alpha > \beta$ and $\map f z = \map \OO {e^{\cmod z^m} }$.
Then:
:$\map g z = \map {\mathcal o} {e^{\cmod z^m} }$
So $\dfrac {\map g z} {e^{\cmod z^m} } \to 0$ as $\cmod z \to \infty$.
In particular:
:$\dfrac {\map f z + \map g z} {e^{\cmod z^m} } \sim \dfrac {\map f z} {e^{\cmod z^m} } > 0$
and minimizing $m$ we see that the order of $f + g$ is at least $\alpha$.
{{ProofWanted}}
Theorem: Exponent of Convergence is Less Than Order

Let $f: \C \to \C$ be an entire function.
Let $\omega$ be its order.
Let $\tau$ be its exponent of convergence.
Then $\tau \le \omega$.

Proof:
We may assume $\map f 0 \ne 0$.
Let $f$ have finitely many zeroes.
Then:
:$\tau = 0 \le \omega$
{{qed|lemma}}
Let $f$ have infinitely many zeroes.
Let $\sequence {a_n}$ be the sequence of nonzero zeroes of $f$, repeated according to multiplicity and ordered by increasing modulus.
Let $r_n = \size {a_n}$ and $R_n = 2 \size {a_n}$.
By Jensen's Inequality:
:$n \le \dfrac {\map \log {\max_{\size z \le R_n} \size f} - \log \size {\map f 0} } {\log 2}$
for all $n \in \N$.
Let $\epsilon > 0$.
Because $f$ has order $\omega$:
:$n \ll_\epsilon \size {a_n}^{\omega + \epsilon}$
Thus:
:$\size {a_n}^{-\paren {\omega + \epsilon} } \ll_\epsilon n^{-1}$
By Convergence of P-Series:
:$\omega + \epsilon \ge \tau$
Because $\epsilon$ is arbitrary:
:$\omega \ge \tau$
{{qed}}
Theorem: Class is Proper iff Bijection from Class to Proper Class/Corollary

$A$ is proper {{iff}} there exists a bijection from $P$ to $A$.

Proof:
{{NotZFC}}
From Biconditional is Transitive and Class is Proper iff Bijection from Class to Proper Class, it suffices to show that:
:There exists a bijection from $A$ to $P$ {{iff}} there exists a bijection from $P$ to $A$.
The rest follows from Inverse of Bijection is Bijection.
{{qed}}
Category:Gödel-Bernays Class Theory
Category:Class Mappings
po94h4njca4vgfd4re167c1t0y7n0uk
Theorem: Length of God's Algorithm for Sam Loyd's Fifteen Puzzle

The length of God's Algorithm for Sam Loyd's Fifteen Puzzle is $52$.

Proof:
{{ProofWanted|A lot of background material needed first.}}
Theorem: Injection from Proper Class to Class

Let $A$ be a class.
Let $P$ be a proper class.
Let $f: P \to A$ be an injection.
Then $A$ is proper.

Proof:
{{NotZFC}}
{{AimForCont}} $A$ is not proper.
Then it must be a set.
By Injection to Image is Bijection, it follows that the restriction $f \restriction_{P \times f \sqbrk P}$ is a bijection.
By the corollary of Class is Proper iff Bijection from Class to Proper Class, $f \sqbrk P$ is proper.
But since $f \sqbrk P \subseteq A$, this contradicts Subclass of Set is Set.
And so by contradiction, $A$ cannot be a set.
Therefore $A$ is proper.
{{qed}}
Category:Gödel-Bernays Class Theory
Category:Class Mappings
p1ckjlth8azbqtjdsct48ef5tsxff4l
Theorem: Polynomial has Order Zero

Let $P: \C \to \C$ be a polynomial function.
Then $P$ has order $0$.

Proof:
Follows from a slightly stronger result than Limit at Infinity of Polynomial over Complex Exponential.
{{ProofWanted}}
Theorem: Period of Reciprocal of 53 is One Quarter of Maximal

The decimal expansion of the reciprocal of $53$ has $\dfrac 1 4$ the maximum period, that is: $13$:
:$\dfrac 1 {53} = 0 \cdotp \dot 01886 \, 79245 \, 28 \dot 3$

Proof:
From Reciprocal of $53$:
{{:Reciprocal of 53}}
Counting the digits, it is seen that this has a period of recurrence of $13$.
From Maximum Period of Reciprocal of Prime, the maximum period of recurrence of $\dfrac 1 p$ is $p - 1$.
We have that:
:$13 = \dfrac {53 - 1} 4$
Hence the result.
{{qed}}
Theorem: Order is Maximum of Exponent of Convergence and Degree

Let $f: \C \to \C$ be an entire function.
Let $\omega$ be its order.
Let $\tau$ be its exponent of convergence.
Let $h$ be the degree of the polynomial in its canonical factorization.
Then:
:$\omega = \map \max {\tau, h}$

Proof:
By Exponent of Convergence is Less Than Order:
:$\tau \le \omega$
By Hadamard Factorization Theorem:
:$h \le \omega$
Thus:
:$\map \max {\tau, h} \le \omega$
By Order is Less Than Maximum of Exponent of Convergence and Degree:
:$\omega \le \map \max {\tau, h}$
{{qed}}
Theorem: Order of Reciprocal of Entire Function

Let $f: \C \to \C$ be an entire function of order $\rho$.
Let $f$ have no zeroes.
Then $1/f$ has order $\rho$.

Proof:
By Zerofree Analytic Function on Simply Connected Set has Logarithm, there exists an entire function $g$ with $f = \exp g$.
{{ProofWanted}}
Theorem: Jacobi's Necessary Condition/Dependent on N Functions

Let $J$ be a functional, such that:
:$J \sqbrk {\mathbf y} = \ds \int_a^b \map F {x, \mathbf y, \mathbf y'} \rd x$
where $\mathbf y = \paren {\sequence {y_i}_{1 \le i \le N} }$ is an N-dimensional real vector.
Let $\map {\mathbf y} x$ correspond to the minimum of $J$.
Let the $N\times N$ matrix $\mathbf P = F_{y_i' y_j'}$ be positive definite along $\map {\mathbf y} x$.
Then the open interval $\openint a b$ contains no points conjugate to $a$.

Proof:
By Necessary Condition for Twice Differentiable N Function dependent Functional to have Minimum, $J$ is minimised by $y = \map {\mathbf {\hat y} } x$ if:
:$\delta^2 J \sqbrk {\mathbf {\hat y}; \mathbf h} \ge 0$ 
for all admissable real functions $\mathbf h$.
By lemma 1 of Legendre's Condition:
:$\ds \delta^2 J \sqbrk {\mathbf y; \mathbf h} = \int_a^b \paren {\mathbf h' \mathbf P \mathbf h' + \mathbf h \mathbf Q \mathbf h} \rd x$
where:
:$\mathbf P = F_{y_i' y_j'}$
By Nonnegative Quadratic N function dependent Functional implies no Interior Conjugate Points, $\openint a b$ does not contain any conjugate points {{WRT}} $J$.
{{qed}}
Theorem: Probability of no 2 People out of 53 Sharing the Same Birthday

Let there be $53$ people in a room.
The probability that no $2$ of them have the same birthday is approximately $\dfrac 1 {53}$.

Proof:
{{Refactor|The analyis has already been performed in Birthday Paradox. Extract that general case and make it a theorem, and then introduce Birthday Paradox and this page as examples.|level = medium}}
Let there be $n$ people in the room.
Let $\map p n$ be the probability that no two people in the room have the same birthday.
For simplicity, let us ignore leap years and assume there are $365$ days in the year.
Let the birthday of person $1$ be established.
The probability that person $2$ shares person $1$'s birthday is $\dfrac 1 {365}$.
Thus, the probability that person $2$ does not share person $1$'s birthday is $\dfrac {364} {365}$.
Similarly, the probability that person $3$ does not share the birthday of either person $1$ or person $2$ is $\dfrac {363} {365}$.
And further, the probability that person $n$ does not share the birthday of any of the people indexed $1$ to $n - 1$ is $\dfrac {365 - \paren {n - 1} } {365}$.
Hence the total probability that none of the $n$ people share a birthday is given by:
:$\map p n = \dfrac {364} {365} \dfrac {363} {365} \dfrac {362} {365} \cdots \dfrac {365 - n + 1} {365}$
{{begin-eqn}}
{{eqn | l = \map p n
      | r = \dfrac {364} {365} \dfrac {363} {365} \dfrac {362} {365} \cdots \dfrac {365 - n + 1} {365}
      | c = 
}}
{{eqn | r = \dfrac {365!} {365^n} \binom {365} n
      | c = 
}}
{{end-eqn}}
Setting $n = 53$ and evaluating the above gives:
:$\map p {53} \approx 0.01887$
or:
:$\map p {53} \approx \dfrac 1 {53.01697}$
{{qed}}
Theorem: Triangular Fibonacci Numbers

The only Fibonacci numbers which are also triangular are:
:$0, 1, 3, 21, 55$
{{OEIS|A039595}}

Proof:
{{begin-eqn}}
{{eqn | l = 0
      | r = \dfrac {0 \times 1} 2
}}
{{eqn | l = 1
      | r = \dfrac {1 \times 2} 2
}}
{{eqn | l = 3
      | r = \dfrac {2 \times 3} 2
      | rr= = 1 + 2
}}
{{eqn | l = 21
      | r = \dfrac {6 \times 7} 2
      | rr= = 8 + 13
}}
{{eqn | l = 55
      | r = \dfrac {10 \times 11} 2
      | rr= = 21 + 34
}}
{{end-eqn}}
It remains to be shown that these are the only ones.
Let $F_n$ be the $n$th Fibonacci number.
From Odd Square is Eight Triangles Plus One, $F_n$ is triangular {{iff}} $8 F_n + 1$ is square.
It remains to be demonstrated that $8 F_n + 1$ is square {{iff}}:
:$n \in \set{\pm 1, 0, 2, 4, 8, 10}$
So, let $8 F_n + 1$ be square.
Then:
:$n \equiv \begin{cases} \pm 1 \pmod {2^5 \times 5} & : n \text { odd} \\ 0, 2, 4, 8, 10 \pmod {2^5 \times 5^2 \times 11} & : n \text { even} \end{cases}$
{{ProofWanted|The proof needs to be studied.}}
Theorem: Repdigit Triangular Numbers

The only repdigit numbers which are also triangular are:
:$55, 66, 666$
{{OEIS|A045914}}

Proof:
{{begin-eqn}}
{{eqn | l = 55
      | r = \dfrac {10 \times 11} 2
}}
{{eqn | l = 66
      | r = \dfrac {11 \times 12} 2
}}
{{eqn | l = 666
      | r = \dfrac {36 \times 37} 2
}}
{{end-eqn}}
Let $\dfrac {d \paren {10^j - 1}} 9$ be a $j$-digit repdigit number.
Suppose it is triangular.
For $d = 1$, write:
{{begin-eqn}}
{{eqn | l = \frac {k \paren {k + 1} } 2
      | r = \frac {10^j - 1} 9
}}
{{eqn | l = 9 k \paren {k + 1}
      | r = 2 \times 10^j - 2
}}
{{eqn | l = \paren {3 k + 1} \paren {3 k + 2}
      | r = 2^{j + 1} \times 5^j
}}
{{end-eqn}}
Since $3 k + 1 \perp 3 k + 2$, one of them is equal to $2^{j + 1}$ while the other is equal to $5^j$.
This gives $2^{j + 1} \pm 1 = 5^j$.
Since $j \ge 1$, taking modulo $4$:
:$0 \pm 1 \equiv 1^j \equiv 1 \pmod 4$
so we have:
:$2^{j + 1} + 1 = 5^j$
By 1 plus Power of 2 is not Perfect Power except 9, the above equation has no solutions for $j > 1$.
For $j = 1$ we have equality.
Hence $1$ is the only triangular repunit.
{{qed|lemma}}
By Odd Square is Eight Triangles Plus One:
:$x = 1 + \dfrac {8 d \paren {10^j - 1}} 9$ is a perfect square.
For $d = 2, 4, 7, 9$, $x$ ends in $2$ or $3$, which is not a perfect square by Square Modulo 5/Corollary.
{{qed|lemma}}
For $d = 3, 8$, $x$ ends in $5$.
Since it is a perfect square, $x$ must end in $25$.
This is satisfied only when $d = 3, j = 1$.
For $d = 3, j > 1$ and $d = 8, j = 1$, $x$ ends in $65$.
For $d = 8, j > 1$, $x$ ends in $05$.
This corresponds to $\dfrac {x - 1} 8 = 3$.
{{qed|lemma}}
For $d = 5$, $x$ is in the form $44 \dots 41$.
We show that $x$ is square only when $x = 441$.
{{finish|see talk}}
This corresponds to $\dfrac {x - 1} 8 = 55$.
{{qed|lemma}}
For $d = 6$, $x$ is either:
:$49$ for $j = 1$
:$53 \dots 329$ for $j > 1$, with $j - 1$ $3$'s
we show that $x$ is square only when $x = 49, 529, 5329$.
{{finish|see talk}}
These correspond to $\dfrac {x - 1} 8 = 6$, $66$ and $666$.
{{qed|lemma}}
We have hence demonstrated that the only triangular repdigit numbers are:
:$1, 3, 6, 55, 66, 666$
Theorem: Increasing and Ordering on Mappings implies Mapping is Composition

Let $L = \struct {S, \preceq}, R = \struct {T, \preccurlyeq}$ be ordered sets.
Let $g: S \to T, d: T \to S$ be mappings such that
:$g$ and $d$ are increasing mappings
and
:$d \circ g \preceq I_S$ and $I_T \preccurlyeq g \circ d$
where $\preceq, \preccurlyeq$ denotes the orderings on mappings.
Then $d = d \circ \paren {g \circ d}$ and $g = \paren {g \circ d} \circ g$

Proof:
Let $t \in T$.
By definition of ordering on mappings:
:$\map {I_T} t \preccurlyeq \map {\paren {g \circ d} } t$
By definition of identity mapping:
:$t \preccurlyeq \map {\paren {g \circ d} } t$
By definition of increasing mapping:
:$\map d t \preceq \map d {\map {\paren {g \circ d} } t}$
By definition of composition of mappings:
:$\map d t \preceq \map {\paren {d \circ \paren {g \circ d} } } t$
By definition of ordering on mappings:
:$\map {\paren {d \circ g} } {\map d t} \preceq \map {I_S} {\map d t}$
By definition of identity mapping:
:$\map {\paren {d \circ g} } {\map d t} \preceq \map d t$
By definition of composition of mappings:
:$\map {\paren {\paren {d \circ g} \circ d} } t \preceq \map d t$
By Composition of Mappings is Associative:
:$\map {\paren {d \circ \paren {g \circ d} } } t \preceq \map d t$
Thus by definition of antisymmetry:
:$\map d t = \map {\paren {d \circ \paren {g \circ d} } } t$
{{qed|lemma}}
Thus $g = \paren {g \circ d} \circ g$ holds by {{mutatis}}.
{{qed}}
Theorem: Closed Form for Square Pyramidal Numbers

The closed-form expression for the $n$th square pyramidal number is:
:$S_n = \dfrac {n \paren {n + 1} \paren {2 n + 1} } 6$

Proof:
{{begin-eqn}}
{{eqn | l = S_n
      | r = \sum_{k \mathop = 1}^n k^2
      | c = {{Defof|Square Pyramidal Number}}
}}
{{eqn | r = \dfrac {n \paren {n + 1} \paren {2 n + 1} } 6
      | c = Sum of Sequence of Squares
}}
{{end-eqn}}
{{qed}}
Theorem: Closed Form for Pentagonal Pyramidal Numbers

The closed-form expression for the $n$th pentagonal pyramidal number is:
:$Q_n = \dfrac {n^2 \paren {n + 1} } 2$

Proof:
{{begin-eqn}}
{{eqn | l = Q_n
      | r = \sum_{k \mathop = 1}^n P_k
      | c = {{Defof|Pentagonal Pyramidal Number}}
}}
{{eqn | r = \sum_{k \mathop = 1}^n \dfrac {k \paren {3 k - 1} } 2
      | c = Closed Form for Pentagonal Numbers
}}
{{eqn | r = \dfrac 1 2 \paren {3 \sum_{k \mathop = 1}^n k^2 - \sum_{k \mathop = 1}^n k}
      | c = 
}}
{{eqn | r = \dfrac 1 2 \paren {3 \frac {n \paren {n + 1} \paren {2 n + 1} } 6 - \sum_{k \mathop = 1}^n k}
      | c = Sum of Sequence of Squares
}}
{{eqn | r = \dfrac 1 2 \paren {3 \frac {n \paren {n + 1} \paren {2 n + 1} } 6 - \dfrac {n \paren {n + 1} } 2}
      | c = Closed Form for Triangular Numbers
}}
{{eqn | r = \dfrac 1 2 \paren {\frac {n \paren {n + 1} \paren {2 n + 1} - n \paren {n + 1} } 2}
      | c = 
}}
{{eqn | r = \dfrac 1 2 \paren {\frac {n \paren {n + 1} \paren {2 n} } 2}
      | c = 
}}
{{eqn | r = \frac {n^2 \paren {n + 1} } 2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Surjection from Class to Proper Class

Let $A$ be a class.
Let $\mathrm P$ be a proper class.
Let $f: A \to \mathrm P$ be a surjection.
Then $A$ is proper.

Proof:
{{AimForCont}} $A$ is not proper.
Then $A$ must be a set.
By the Axiom of Powers, $\powerset A$ is also a set.
Let $g: f \sqbrk A \to \powerset A$ be defined as:
:$\map g {\map f a} = f^{-1} \sqbrk {\set {\map f a} }$
It should be noted that:
:$\forall a \in A: \map {\paren {g \circ f} } a \ne \O$:
Suppose that $\map g {\map f a} = \map g {\map f b}$.
Let $x \in f^{-1} \sqbrk {\set {\map f a} }$.
Then by the definition of a singleton:
:$x \in f^{-1} \sqbrk {\set {\map f a} } \implies \map f x \in \set {\map f a} \implies \map f x = \map f a$
By the same argument:
:$x \in f^{-1} \sqbrk {\set {\map f b} } \implies \map f x = \map f b$
Hhence by the properties of equality:
:$\map f a = \map f b$
It has been shown that $g$ is an injection.
Because $f$ is a surjection, it follows by definition of surjection that:
:$f \sqbrk A = \mathrm P$
But this contradicts Injection from Proper Class to Class.
Thus by contradiction $A$ must be proper.
Hence the result.
{{qed}}
Category:Gödel-Bernays Class Theory
Category:Class Mappings
6j4n94vdzsf85go4zenhrfrkoxk6rva
Theorem: Image of Set under Mapping is Set

Let $A$ be a class.
Let $\mathrm U$ denote the universal class.
Let $f: A \to \mathrm U$ be a class mapping.
Let $S$ be a subset of $A$.
{{explain|Note that further work is needed on the Subset page to clarify that a "subset" of a "proper class" is indeed a "set". Some words are already on that page, but this needs to be formalised and separated out into its own transcluded "class theoretic" page.}}
Then the image $f \sqbrk S$ is also a set.
If $A$ is a set, then this result is known as the Axiom of Replacement in Zermelo-Fraenkel set theory.

Proof:
{{NotZFC}}
{{AimForCont}} $f \sqbrk S$ is not a set.
Then $f \sqbrk S$ must be proper.
By Restriction of Mapping to Image is Surjection, the restriction $f \restriction_{S \times f \sqbrk S}$ is a surjection.
But this contradicts Surjection from Class to Proper Class.
Thus by contradiction, $f \sqbrk S$ is a set.
Hence the result.
{{qed}}
Category:Gödel-Bernays Class Theory
Category:Class Mappings
99s9rd9db3t8ipugvk18aa1tdrxrcpi