avewright/proofwiki-math huggingface dataset:
Theorem: Dilogarithm Reflection Formula

:$\map {\Li_2} z + \map {\Li_2} {1 - z} = \map \zeta 2 - \map \ln z \map \ln {1 - z}$

Proof:
From the definition of the dilogarithm function:
:$\ds \map {\Li_2} z = -\int_0^z \dfrac {\map \ln {1 - x} } x \rd x$
With a view to expressing the primitive in the form:
:$\ds \int u \frac {\d v} {\d x} \rd x = u v - \int v \frac {\d u} {\d x} \rd x$
let:
{{begin-eqn}}
{{eqn | l = u
      | r = \map \ln {1 - x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = -\frac 1 {1 - x}
      | c = Derivative of $\ln x$, Chain Rule
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = \frac 1 x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \map \ln x
      | c = Primitive of Reciprocal
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = -\int_0^z \dfrac {\map \ln {1 - x} } x \rd x
      | r = -\paren {\bigintlimits {\map \ln {1 - x} \map \ln x} 0 z   + \int_0^z \frac {\map \ln x} {1 - x} \rd x}
      | c = Integration by Parts
}}
{{eqn | r = -\map \ln z \map \ln {1 - z} - \int_0^z \frac {\map \ln x} {1 - x} \rd x
      | c = simplifying
}}
{{eqn | r = -\map \ln z \map \ln {1 - z} + \int_1^{1 - z} \dfrac {\map \ln {1 - t} } t \rd t
      | c = $\paren {1 - x} \to t$ and $\rd x \to -\rd t$
}}
{{eqn | r = -\map \ln z \map \ln {1 - z} - \paren {\map {\Li_2} {1 - z} - \map {\Li_2} 1}
      | c = {{Defof|Dilogarithm Function}}
}}
{{eqn | r = -\map \ln z \map \ln {1 - z} - \map {\Li_2} {1 - z} + \map {\Li_2} 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {\Li_2} z + \map {\Li_2} {1 - z}
      | r = -\map \ln z \map \ln {1 - z} - \map {\Li_2} {1 - z} + \map {\Li_2} 1 +  \map {\Li_2} {1 - z}
      | c = 
}}
{{eqn | r = \map \zeta 2 - \map \ln z \map \ln {1 - z}
      | c = Dilogarithm of One
}}
{{end-eqn}}
{{qed}}
Theorem: Dilogarithm of Minus One

:$\map {\Li_2} {-1} = -\dfrac 1 2 \map \zeta 2$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\Li_2} z
      | r = \sum_{n \mathop = 1}^\infty \frac {z^n} {n^2}
      | c = Power Series Expansion for Spence's Function
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^n} {n^2}
      | c = $z := -1$
}}
{{eqn | r = - \map \eta 2
      | c = {{Defof|Dirichlet Eta Function}}
}}
{{eqn | r = - \paren {1 - 2^{1 - 2} } \map \zeta 2
      | c = Riemann Zeta Function in terms of Dirichlet Eta Function
}}
{{eqn | r = -\dfrac 1 2 \map \zeta 2
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Examples of Dilogarithm Function
Category:Spence's Function
nv316o102na5625h2432vl7b21hnzi0
Theorem: Dilogarithm of One Half

:$\map {\Li_2} {\dfrac 1 2} = \dfrac 1 2 \paren {\map \zeta 2 - \paren {\map \ln 2}^2}$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\Li_2} z + \map {\Li_2} {1 - z}
      | r = \map \zeta 2 - \map \ln z \map \ln {1 - z}
      | c = Dilogarithm Reflection Formula
}}
{{eqn | ll = \leadsto
      | l = \map {\Li_2} {\frac 1 2} + \map {\Li_2} {\frac 1 2}
      | r = \map \zeta 2 - \map \ln {\frac 1 2} \map \ln {\frac 1 2}
      | c = $z := \dfrac 1 2$
}}
{{eqn | ll = \leadsto
      | l = 2 \map {\Li_2} {\frac 1 2}
      | r = \map \zeta 2 - \paren {\map \ln {\frac 1 2} }^2
      | c = 
}}
{{eqn | r = \dfrac 1 2 \paren {\map \zeta 2 - \paren {-\map \ln 2}^2}
      | c = Logarithm of Reciprocal and dividing by $2$
}}
{{eqn | r = \dfrac 1 2 \paren {\map \zeta 2 - \paren {\map \ln 2}^2}
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Examples of Dilogarithm Function
Category:Spence's Function
mdgz3b3y5iobng3u3po7xinpsybj4qw
Theorem: Dilogarithm of Minus Z Plus Dilogarithm of Minus Reciprocal of Z

:$\map {\Li_2} {-z} + \map {\Li_2} {-\dfrac 1 z} = -\map \zeta 2 - \dfrac 1 2 \map {\ln^2} z$

Proof:
From the definition of the dilogarithm function:
:$\ds \map {\Li_2} z = -\int_0^z \dfrac {\map \ln {1 - x} } x \rd x$
Taking the derivative of both sides at $-\dfrac 1 z$
{{begin-eqn}}
{{eqn | l = \frac \d {\d z} \map {\Li_2} {-\dfrac 1 z}
      | r = -\paren {\dfrac {\map \ln {1 - \paren {-\dfrac 1 z} } } {\paren {-\dfrac 1 z} } \paren {\dfrac 1 {z^2} } }
      | c = $x \to -\dfrac 1 z$ and $\rd x \to \dfrac 1 {z^2}$ Derivative of Reciprocal
}}
{{eqn | r = \dfrac {\map \ln {1 + \dfrac 1 z} } z
      | c = 
}}
{{eqn | r = \dfrac {\map \ln {\dfrac {z + 1} z} } z
      | c = 
}}
{{eqn | r = \dfrac {\map \ln {z + 1} - \map \ln z} z
      | c = Difference of Logarithms
}}
{{end-eqn}}
Now integrating both sides {{WRT|Integration}} $z$, we obtain:
{{begin-eqn}}
{{eqn | l = \int_0^z \frac \d {\d z} \map {\Li_2} {-\dfrac 1 z}
      | r = \int_0^z \dfrac {\map \ln {z + 1} - \map \ln z} z \rd z
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {\Li_2} {-\dfrac 1 z}
      | r = \int_0^z \dfrac {\map \ln {z + 1} } z \rd z - \int_0^z \dfrac {\map \ln z} z \rd z
      | c = Fundamental Theorem of Calculus and Linear Combination of Definite Integrals
}}
{{eqn | r = \int_0^z \dfrac {\map \ln {1 - \paren {-z} } } z \rd z - \int_0^z \dfrac {\map \ln z} z \rd z
      | c = 
}}
{{eqn | r = -\map {\Li_2} {-z} - \int_0^z \dfrac {\map \ln z} z \rd z
      | c = {{Defof|Dilogarithm Function}}
}}
{{eqn | ll= \leadsto
      | l = \map {\Li_2} {-z} + \map {\Li_2} {-\dfrac 1 z}
      | r = -\int_0^z \dfrac {\map \ln z } z \rd z
      | c = 
}}
{{eqn | r = -\paren {\frac {\ln^2 z} 2 + C }
      | c = Primitive of Logarithm of x over x
}}
{{end-eqn}}
We now solve for $C$ by setting $z = 1$
{{begin-eqn}}
{{eqn | l = \map {\Li_2} {-1} + \map {\Li_2} {-1}
      | r = -\paren {\frac {\ln^2 1} 2 + C }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = -\dfrac 1 2 \map \zeta 2 + -\dfrac 1 2 \map \zeta 2
      | r = -\paren {0 + C}
      | c = Dilogarithm of Minus One and Natural Logarithm of 1 is 0
}}
{{eqn | ll= \leadsto
      | l = -\map \zeta 2
      | r = -C
      | c = 
}}
{{end-eqn}}
Therefore:
:$\map {\Li_2} {-z} + \map {\Li_2} {-\dfrac 1 z} = -\map \zeta 2 - \dfrac 1 2 \map {\ln^2} z$
{{qed}}
Theorem: Dilogarithm of Zero

:$\map {\Li_2} 0 = 0$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\Li_2} z
      | r = \sum_{n \mathop = 1}^\infty \frac {z^n} {n^2}
      | c = Power Series Expansion for Spence's Function
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty \frac {0^n} {n^2}
      | c = $z := 0$
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Examples of Dilogarithm Function
Category:Spence's Function
rxt8oevskrft0vr7rybkf7xvtiayp68
Theorem: Dilogarithm of One Minus Z Plus Dilogarithm of One Minus Reciprocal of Z

:$\map {\Li_2} {1 - z} + \map {\Li_2} {1 - \dfrac 1 z} = -\dfrac 1 2 \map {\ln^2} z$

Proof:
From the definition of the dilogarithm function:
:$\ds \map {\Li_2} z = -\int_0^z \dfrac {\map \ln {1 - x} } x \rd x$
Taking the derivative of both sides at $-\dfrac z {1 - z}$
{{begin-eqn}}
{{eqn | l = \frac {\d } {\d z} \map {\Li_2} {-\dfrac z {1 - z} }
      | r = -\paren {\dfrac {\map \ln {1 - \paren {-\dfrac z {1 - z} } } } {\paren {-\dfrac z {1 - z} } } \paren {-\dfrac 1 {\paren {1 - z}^2} } }
      | c = $x \to -\dfrac z {1 - z}$ and $\rd x \to -\dfrac 1 {\paren {1 - z}^2}$
}}
{{eqn | r = \dfrac {-\map \ln {\dfrac {1 - z} {1 -z} + \dfrac z {1 -z} } } {z \paren {1 - z} }
      | c = 
}}
{{eqn | r = \dfrac {-\map \ln {\dfrac 1 {1 -z} } } {z \paren {1 - z} }
      | c = 
}}
{{eqn | r = \dfrac {-\paren {\map \ln 1 - \map \ln {1 - z} } } {z \paren {1 - z} }
      | c = Difference of Logarithms
}}
{{eqn | r = \dfrac {-\map \ln 1 } {z \paren {1 - z} } + \dfrac {\map \ln {1 - z} } {z \paren {1 - z} }
      | c = 
}}
{{eqn | r = \dfrac {\map \ln {1 - z} } {z \paren {1 - z} }
      | c = Natural Logarithm of 1 is 0
}}
{{eqn | r = \dfrac {\map \ln {1 - z} } {\paren {1 - z} } + \dfrac {\map \ln {1 - z} } z
      | c = 
}}
{{end-eqn}}
Now integrating both sides {{WRT|Integration}} $z$, we obtain:
{{begin-eqn}}
{{eqn | l = \int_0^z \frac \d {\d z} \map {\Li_2} {-\dfrac z {1 - z} }
      | r = \int_0^z \paren {\dfrac {\map \ln {1 - z} } {\paren {1 - z} } + \dfrac {\map \ln {1 - z} } z} \rd z
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {\Li_2} {-\dfrac z {1 - z} }
      | r = \int_0^z \dfrac {\map \ln {1 - z} } {\paren {1 - z} } \rd z + \int_0^z \dfrac {\map \ln {1 - z} } z \rd z
      | c = Fundamental Theorem of Calculus and Linear Combination of Definite Integrals
}}
{{eqn | r = \int_0^z \dfrac {\map \ln {1 - z} } {\paren {1 - z} } \rd z - \map {\Li_2} z
      | c = {{Defof|Dilogarithm Function}}
}}
{{eqn | ll= \leadsto
      | l = \map {\Li_2} z + \map {\Li_2} {-\dfrac z {1 - z} }
      | r = \int_0^z \dfrac {\map \ln {1 - z} } {\paren {1 - z} } \rd z
      | c = 
}}
{{eqn | r = \int_1^{1 - z} \dfrac {\map \ln u } u \paren {-\rd u}
      | c = $\paren {1 - z} \to u$ and $\rd z \to -\rd u$ U-Substitution
}}
{{eqn | r = -\frac 1 2 \map {\ln^2} {1 - z} + C
      | c = Primitive of Logarithm of x over x
}}
{{end-eqn}}
We now solve for $C$ by setting $z = 0$
{{begin-eqn}}
{{eqn | l = \map {\Li_2} 0 + \map {\Li_2} 0
      | r = -\frac 1 2 \ln^2 1 + C
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 0
      | r = 0 + C
      | c = Dilogarithm of Zero and Natural Logarithm of 1 is 0
}}
{{eqn | ll= \leadsto
      | l = 0
      | r = C
      | c = 
}}
{{end-eqn}}
Therefore:
{{begin-eqn}}
{{eqn | l = \map {\Li_2} z + \map {\Li_2} {-\dfrac z {1 - z} }
      | r = -\frac 1 2 \map {\ln^2} {1 - z}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {\Li_2} {1 - z} + \map {\Li_2} {1 - \dfrac 1 z}
      | r = -\frac 1 2 \map {\ln^2} z
      | c = $z \to \paren {1 - z}$
}}
{{end-eqn}}
{{qed}}
Theorem: Complement of Singleton Closure is Meet-Irreducible

Let $\struct {S, \tau}$ be a topological space.
Let $x \in S$.
Then:
:$S \setminus \set x^-$ is a meet-irreducible open set
where $\set x^-$ denotes the closure of $\set x$

Proof:
From Characterization of Meet-Irreducible Open Set:
$S \setminus \set x^-$ is a '''meet-irreducible open set''' {{iff}}
:$\forall U, V \in \tau : \paren {U \cap V \subseteq S \setminus \set x^- \implies U \subseteq S \setminus \set x^- \text { or } V \subseteq S \setminus \set x^-}$
Let:
:$U, V \in \tau: U \cap V \subseteq S \setminus \set x^-$
By Set is Subset of its Topological Closure:
:$x \in \set x^-$
By definition of set difference:
:$x \notin S \setminus \set x^-$
By definition of subset:
:$x \notin U \cap V$
By definition of set intersection:
:either $x \notin U$ or $x \notin V$
{{WLOG}}, suppose $x \notin U$.
By definition of set complement:
:$x \in S \setminus U$
We have $S \setminus U$ is a closed set by definition.
From Closure of Subset of Closed Set of Topological Space is Subset:
:$\set x^- \subseteq S \setminus U$
From Subset of Set Difference iff Disjoint Set:
:$U \subseteq S \setminus \set x^-$
The result follows.
{{qed}}
Theorem: Existence of Class Intersection

For any classes $X, Y$, the intersection $X \cap Y$ exists and is unique.
That is:
:$\forall X, Y: \exists! Z: \forall u: u \in Z \iff u \in X \land u \in Y$
where $X \cap Y := Z$.

Proof:
Let $X, Y$ be arbitrary.
By Axiom $\text B 2$, there is some class $Z$ such that:
:$\forall u: u \in Z \iff u \in X \land u \in Y$
satisfying the existence portion of the theorem.
{{qed|lemma}}
Now, let some $Z'$ satisfy:
:$\forall u: u \in Z' \iff u \in X \land u \in Y$
For each set $u$:
:$u \in Z \iff u \in X \land u \in Y \iff u \in Z'$
and thus:
:$u \in Z \iff u \in Z'$
Thus, by Axiom of Extension:
:$Z = Z'$
satisfying the uniqueness portion of the theorem.
{{qed}}
Category:Class Theory
Category:Von Neumann-Bernays-Gödel Set Theory
9y1gl8lqfc5kps4ff9v7swtsk4tplwq
Theorem: Existence of Class Complement

Let $X$ be a class.
Then there is a unique class $Z$ such that, for every set $u$:
:$u \in Z \iff u \notin X$

Proof:
Let $X$ be arbitrary.
By Axiom $\text B 3$, there is a class $Z$ such that:
:$\forall u: u \in Z \iff u \notin X$
This satisfies the existence portion of the theorem.
{{qed|lemma}}
Let $Z'$ be a class such that:
:$\forall u: u \in Z' \iff u \notin X$
Then, for every set $u$:
:$u \in Z \iff u \notin X \iff u \in Z'$
Therefore, by the Axiom of Extension:
:$Z = Z'$
satisfying the uniqueness portion of the theorem.
{{qed}}
Category:Class Theory
Category:Von Neumann-Bernays-Gödel Set Theory
c9po2we97rg0ynm42ph43akh66zr6du
Theorem: Sober Space is T0

Let $\struct {S, \tau}$ be a sober space.
Then:
:$\struct {S, \tau}$ is a $T_0$ (Kolmogorov) space.

Proof:
Let $x, y \in S : x \ne y$.
From Complement of Singleton Closure is Meet-Irreducible:
:$S \setminus \set x^-$ is a meet-irreducible open set
By definition of a sober space:
:$S \setminus \set x^-$ is uniquely defined by $x$
Hence:
:$S \setminus \set x^- \ne S \setminus \set y^-$
From Equal Relative Complements iff Equal Subsets:
:$\set x^- \ne \set y^-$
Since $x, y$ were arbitrary, it follows that:
:$\forall x, y \in S : x \ne y \implies \set x^- \ne \set y^-$
From Characterization of T0 Space by Distinct Closures of Singletons:
:$\struct {S, \tau}$ is a $T_0$ (Kolmogorov) space
{{qed}}
Theorem: T2 Space is Sober Space

Let $\struct {S, \tau}$ be a $T_2$ (Hausdorff) space.
Then:
:$\struct {S, \tau}$ is a sober space.

Proof:
Let $W \in \tau$ be meet-irreducible open proper subset of $S$.
Let $x \in S \setminus W$.
We have $S \setminus W$ is a closed set by definition.
From Closure of Subset of Closed Set of Topological Space is Subset:
:$\set x^- \subseteq S \setminus W$
From Relative Complement inverts Subsets of Relative Complement:
:$W \subseteq S \setminus \set x^-$
Hence:
:$x \notin W$
Let $y \in S \setminus \set x^-$.
Then:
:$y \ne x$
By definition of $T_2$ (Hausdorff) space:
:$\exists W_1, W_2 \in \tau : x \in W_1, y \in W_2 : W_1 \cap W_2 = \O$
Let:
:$U = W \cup W_1$
and
:$V = W \cup W_2$
Hence:
:$x \in U, y \in V$
Since $x \notin W$ and $x \in U$:
:$U \nsubseteq W$
We have:
{{begin-eqn}}
{{eqn | l = U \cap V
      | r = \paren {W \cup W_1} \cap \paren {W \cup W_2}
      | c = Definition of $U$ and $V$
}}
{{eqn | r = \paren {W \cap W} \cup \paren {W \cap W_2} \cup \paren {W_1 \cap W} \cup \paren {W_1 \cap W_2}
      | c = Intersection Distributes over Union
}}
{{eqn | r = W \cup \paren {W \cap W_2} \cup \paren {W_1 \cap W} \cup \paren {W_1 \cap W_2}
      | c = Set Intersection is Idempotent
}}
{{eqn | r = W \cup \paren {W \cap W_2} \cup \paren {W_1 \cap W} \cup \O
      | c = as $W_1 \cap W_2 = \O$
}}
{{eqn | r = W
      | c = Union with Superset is Superset
}}
{{end-eqn}}
From Characterization of Meet-Irreducible Open Set:
:$V = W$
Hence:
:$y \in W$
Since $y$ was arbitrary:
:$S \setminus \set x^- \subseteq W$
By definition of set equivalence:
:$W = S \setminus \set x^-$
{{qed}}
Theorem: Dilogarithm of Minus Reciprocal of Golden Mean

:$\map {\Li_2} {-\dfrac 1 \phi} = -\dfrac 2 5 \map \zeta 2 + \dfrac 1 2 \paren {\map \ln \phi}^2$

Proof:
We now note:
{{begin-eqn}}
{{eqn | l = \map {\Li_2} {1 - z} + \map {\Li_2} {1 - \dfrac 1 z}
      | r = -\dfrac 1 2 \map {\ln^2} z
      | c = Dilogarithm of One Minus Z Plus Dilogarithm of One Minus Reciprocal of Z
}}
{{eqn | ll= \leadsto
      | l = \map {\Li_2} {1 - \frac 1 \phi} + \map {\Li_2} {1 - \dfrac 1 {\frac 1 \phi} }
      | r = -\dfrac 1 2 \map {\ln^2} {\frac 1 \phi}
      | c = setting $z := \dfrac 1 \phi$
}}
{{eqn | ll= \leadsto
      | l = \map {\Li_2} {1 - \frac 1 \phi} + \map {\Li_2} {1 - \phi}
      | r = -\dfrac 1 2 \paren {\map \ln 1 - \map \ln \phi}^2
      | c = Difference of Logarithms
}}
{{eqn | ll= \leadsto
      | l = \map {\Li_2} {1 - \frac 1 \phi} + \map {\Li_2} {-\frac 1 \phi}
      | r = -\dfrac 1 2 \map {\ln^2} \phi
      | c = Natural Logarithm of 1 is 0 and Reciprocal Form of One Minus Golden Mean
}}
{{eqn | ll= \leadsto
      | l = \paren {\dfrac 2 5 \map \zeta 2 - \paren {\map \ln \phi}^2} + \map {\Li_2} {-\frac 1 \phi}
      | r = -\dfrac 1 2 \map {\ln^2} \phi
      | c = Dilogarithm of One Minus Reciprocal of Golden Mean
}}
{{eqn | ll= \leadsto
      | l = \map {\Li_2} {-\dfrac 1 \phi}
      | r = -\dfrac 2 5 \map \zeta 2 + \dfrac 1 2 \paren {\map \ln \phi}^2
      | c = rearranging
}}
{{end-eqn}}
{{qed}}
Theorem: Dilogarithm of Reciprocal of Golden Mean

:$\map {\Li_2} {\dfrac 1 \phi} = \dfrac 3 5 \map \zeta 2 - \paren {\map \ln \phi}^2$

Proof:
We first note the following:
{{begin-eqn}}
{{eqn | l = -\frac 1 \phi
      | r = 1 - \phi
      | c = Reciprocal Form of One Minus Golden Mean
}}
{{eqn | ll= \leadsto
      | n = 1
      | l = \frac 1 {\phi^2}
      | r = 1 - \dfrac 1 \phi
      | c = dividing through by $-\phi$ and rearranging
}}
{{end-eqn}}
We now note:
{{begin-eqn}}
{{eqn | l = \map {\Li_2} z + \map {\Li_2} {-z}
      | r = \dfrac 1 2 \map {\Li_2} {z^2}
      | c = Dilogarithm of Square
}}
{{eqn | ll= \leadsto
      | l = \map {\Li_2} {\frac 1 \phi} + \map {\Li_2} {-\frac 1 \phi}
      | r = \dfrac 1 2 \map {\Li_2} {\frac 1 {\phi^2} }
      | c = setting $z := \dfrac 1 \phi$
}}
{{eqn | ll= \leadsto
      | l = \map {\Li_2} {\dfrac 1 \phi}
      | r = \dfrac 1 2 \map {\Li_2} {1 - \dfrac 1 \phi} - \map {\Li_2} {-\frac 1 \phi}
      | c = substituting $\paren {1}$ above
}}
{{eqn | r = \dfrac 1 2 \paren {\dfrac 2 5 \map \zeta 2 - \paren {\map \ln \phi}^2} - \paren {-\dfrac 2 5 \map \zeta 2 + \dfrac 1 2 \paren {\map \ln \phi}^2}
      | c = Dilogarithm of One Minus Reciprocal of Golden Mean and Dilogarithm of Minus Reciprocal of Golden Mean
}}
{{eqn | ll= \leadsto
      | l = \map {\Li_2} {\dfrac 1 \phi}
      | r = \dfrac 3 5 \map \zeta 2 - \paren {\map \ln \phi}^2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Dilogarithm of Minus Golden Mean

:$\map {\Li_2} {-\phi} = -\dfrac 3 5 \map \zeta 2 - \paren {\map \ln \phi}^2$

Proof:
We now note:
{{begin-eqn}}
{{eqn | l = \map {\Li_2} {-z} + \map {\Li_2} {-\dfrac 1 z}
      | r = -\map \zeta 2 - \dfrac 1 2 \map {\ln^2} z
      | c = Dilogarithm of Minus Z Plus Dilogarithm of Minus Reciprocal of Z
}}
{{eqn | ll= \leadsto
      | l = \map {\Li_2} {-\frac 1 \phi} + \map {\Li_2} {-\dfrac 1 {\frac 1 \phi} }
      | r = -\map \zeta 2 - \dfrac 1 2 \map {\ln^2} {\frac 1 \phi}
      | c = setting $z := \dfrac 1 \phi$
}}
{{eqn | ll= \leadsto
      | l = \map {\Li_2} {-\frac 1 \phi} + \map {\Li_2} {-\phi}
      | r = -\map \zeta 2 - \dfrac 1 2 \paren {\map \ln 1 - \map \ln \phi}^2
      | c = Difference of Logarithms
}}
{{eqn | ll= \leadsto
      | l = \map {\Li_2} {-\frac 1 \phi} + \map {\Li_2} {-\phi}
      | r = -\map \zeta 2 - \dfrac 1 2 \map {\ln^2} \phi
      | c = Natural Logarithm of 1 is 0
}}
{{eqn | ll= \leadsto
      | l = \paren {-\dfrac 2 5 \map \zeta 2 + \dfrac 1 2 \paren {\map \ln \phi}^2 } + \map {\Li_2} {-\phi}
      | r = -\map \zeta 2 - \dfrac 1 2 \map {\ln^2} \phi
      | c = Dilogarithm of Minus Reciprocal of Golden Mean
}}
{{eqn | ll= \leadsto
      | l = \map {\Li_2} {-\phi}
      | r = -\dfrac 3 5 \map \zeta 2 - \paren {\map \ln \phi}^2
      | c = rearranging
}}
{{end-eqn}}
{{qed}}
Theorem: Erdős-Moser Equation

The '''Erdős-Moser Equation''' is the Diophantine equation:
{{begin-eqn}}
{{eqn | l = \sum_{j \mathop = 1}^k j^p
      | r = 1 + 2^p + 3^p + \cdots + k^p
      | c = 
}}
{{eqn | r = \paren {k + 1}^p
      | c = 
}}
{{end-eqn}}
where $k, p \in \N$.
Its only solution is $k = 2$ and $p = 1$:
:$1^1 + 2^1 = 3^1$
{{questionable|This is identified on Wikipedia (hwoever reliable that is) as being unsolved? How certain are we that the above is correct?}}

Proof:
Let $\map {B_n} x$ denote the $n$th Bernoulli polynomial:
:$\ds \map {B_n} x = \sum_{k \mathop = 0}^n \binom n k b_{n - k} x^k$
where $b_n$ denotes the $n$th Bernoulli number.
Theorem: Existence of Domain of Class Relation

Let $X$ be a class.
Then there is a unique class $Z$ such that:
:$\forall u: u \in Z \iff \exists v: \tuple {u, v} \in X$
where $\tuple {\cdot, \cdot}$ represents the Kuratowski formalization of ordered pairs.
That is, $Z$ is the class of all $z$ which appear as the first coordinate of an ordered pair in $X$.

Proof:
Let $X$ be arbitrary.
By Axiom $\text B 4$, there is a class $Z$ such that:
:$\forall u: u \in Z \iff \exists v: \tuple {u, v} \in X$
This satisfies the existence portion of the theorem.
{{qed|lemma}}
Let $Z'$ be a class such that:
:$\forall u: u \in Z' \iff \exists v: \tuple {u, v} \in X$
Then, for every set $u$:
:$u \in Z \iff \paren {\exists v: \tuple {u, v} \in X} \iff u \in Z'$
Therefore, by Axiom of Extension:
:$Z = Z'$
satisfying the uniqueness portion of the theorem.
{{qed}}
Category:Class Theory
Category:Von Neumann-Bernays-Gödel Set Theory
pnbkovo2ayfpk3vw97gds4fjywv4mvn
Theorem: Existence of Class Union

For any classes $X, Y$, the union $X \cup Y$ exists and is unique.
That is:
:$\forall X, Y: \exists! Z: \forall u: u \in Z \iff u \in X \lor u \in Y$
where $X \cup Y := Z$.

Proof:
By Existence of Class Complement, there exist unique classes $\overline X, \overline Y$ such that:
:$u \in \overline X \iff u \notin X$
:$u \in \overline Y \iff u \notin Y$
for all sets $u$.
Then, by Existence of Class Intersection, there is a unique class $\overline X \cap \overline Y$ such that:
:$u \in \overline X \cap \overline Y \iff u \in \overline X \land u \in \overline Y$
By the equivalences above:
:$u \in \overline X \cap \overline Y \iff u \notin X \land u \notin Y$
Finally, by Existence of Class Complement, there is a unique class $\overline {\overline X \cap \overline Y}$ such that:
:$u \in \overline {\overline X \cap \overline Y} \iff u \notin \overline X \cap \overline Y$
By the equivalence above:
:$u \in \overline {\overline X \cap \overline Y} \iff \neg \paren {u \notin X \land u \notin Y}$
But then, by De Morgan's Laws:
:$u \in \overline {\overline X \cap \overline Y} \iff u \in X \lor u \in Y$
Therefore, $Z := \overline {\overline X \cap \overline Y}$ exists and is unique.
{{qed}}
Category:Class Theory
Category:Von Neumann-Bernays-Gödel Set Theory
fkqwgydohc1eupm2vruh7gyrywob0x3
Theorem: Existence of Universal Class

There exists a unique class $V$ such that:
:$\forall u: u \in V$
That is, the universal class exists and is unique.

Proof:
By Existence of Empty Class, there is a unique class $\O$ such that:
:$\forall u: u \notin \O$
for every set $u$.
Thus, by Existence of Class Complement, there is a unique class $\overline \O$ such that:
:$u \in \overline \O \iff u \notin \O$
But then, by the definition of $\O$:
:$\forall u: u \in \overline \O$
Then, $V := \overline \O$ satisfies the theorem, and is unique.
{{qed}}
Category:Class Theory
Category:Von Neumann-Bernays-Gödel Set Theory
ak1y247lmhuxr6jtp1h9qq3tjkkd135