avewright/proofwiki-math huggingface dataset:
Theorem: Arctangent of One

:$\map \arctan 1 = \dfrac \pi 4$

Proof:
By definition, $\arctan$ is the inverse of the tangent function's restriction to $\openint {-\dfrac \pi 2} {\dfrac \pi 2}$. 
By Tangent of $45 \degrees$: 
:$\tan \dfrac \pi 4 = 1$.
As $\dfrac \pi 4 \in \openint {-\dfrac \pi 2} {\dfrac \pi 2}$, we have by the definition of an inverse function: 
:$\map \arctan 1 = \dfrac \pi 4$
{{qed}}
Category:Arctangent Function
anplraa3nd15l4kml36tog79cn8hcgi
Theorem: Sum of Arctangents/Corollary

Let $n \in \N_{>0}$ where $\N_{>0}$ denotes the non-zero natural numbers.
Then: 
:$\ds \map \arctan {\frac 1 n} + \map \arctan {\frac {n - 1} {n + 1} } = \frac \pi 4$
where $\arctan$ denotes the arctangent.

Proof:
{{begin-eqn}}
{{eqn | l = \arctan a + \arctan b
      | r = \map \arctan {\dfrac {a + b} {1 - a b} }
      | c = Sum of Arctangents
}}
{{eqn | ll= \leadsto
      | l = \map \arctan {\dfrac 1 n} + \map \arctan {\dfrac {n - 1} {n + 1} }
      | r = \map \arctan {\dfrac {\dfrac 1 n + \dfrac {n - 1} {n + 1} } {1 - \paren {\dfrac 1 n} \paren {\dfrac {n - 1} {n + 1} } } }
      | c = where $a := \dfrac 1 n$ and $b := \dfrac {n - 1} {n + 1}$
}}
{{eqn | r = \map \arctan {\dfrac {\dfrac {\paren {n + 1 + n^2 - n} } {n \paren {n + 1} } } {\dfrac {\paren {n^2 + n - n + 1} } {n \paren {n + 1} } } }
      | c = 
}}
{{eqn | r = \map \arctan 1
      | c = 
}}
{{eqn | r = \frac \pi 4
      | c = Arctangent of One
}}
{{end-eqn}}
{{qed}}
Category:Sum of Arctangents
Category:Arctangent Function
1i3az8k2uvhasmruz68bzkszbuoqfsb
Theorem: Digamma Function of One Third

:$\map \psi {\dfrac 1 3} = -\gamma - \dfrac 3 2 \ln 3 - \dfrac \pi {2 \sqrt 3}$

Proof:
{{begin-eqn}}
{{eqn | l = \map \psi {\frac 1 3}
      | r = -\gamma - \ln 6 - \frac \pi 2 \map \cot {\frac 1 3 \pi} + 2 \sum_{n \mathop = 1}^{\ceiling {3 / 2} - 1} \map \cos {\frac {2 \pi n} 3} \map \ln {\map \sin {\frac {\pi n} 3} }
      | c = Gauss's Digamma Theorem
}}
{{eqn | r = -\gamma - \ln 2 - \ln 3 - \frac \pi 2 \paren {\frac 1 {\sqrt 3} } + 2 \paren {-\frac 1 2} \map \ln {\frac {\sqrt 3} 2 }
      | c = {{cot|60}}, {{cos|120}}, {{sin|60}} and Sum of Logarithms
}}
{{eqn | r = -\gamma - \ln 2 - \ln 3 - \frac \pi 2 \paren {\frac 1 {\sqrt 3} } - \paren {\frac 1 2 \ln 3 - \ln 2}
      | c = Difference of Logarithms and Logarithm of Power
}}
{{eqn | r = -\gamma - \dfrac 3 2 \ln 3 - \dfrac {\pi} {2 \sqrt 3}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Digamma Function of One Third

:$\map \psi {\dfrac 1 3} = -\gamma - \dfrac 3 2 \ln 3 - \dfrac \pi {2 \sqrt 3}$

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 1}^{n - 1} \map \psi {\frac k n}
      | r = -\paren {n - 1} \gamma - n \ln n
      | c = {{Corollary|Digamma Additive Formula}}
}}
{{eqn | ll= \leadsto
      | l = \sum_{k \mathop = 1}^{3 - 1} \map \psi {\frac k 3}
      | r = -\paren {3 - 1} \gamma - 3 \ln 3
      | c = 
}}
{{eqn | ll= \leadsto
      | n = 1
      | l = \map \psi {\frac 1 3} + \map \psi {\frac 2 3}
      | r = -2 \gamma - 3 \ln 3
      | c = 
}}
{{eqn | n = 2
      | l = \map \psi {\frac 1 3} - \map \psi {\frac 2 3}
      | r = -\pi \map \cot {\frac \pi 3}
      | c = Digamma Reflection Formula
}}
{{eqn | ll= \leadsto
      | l = 2 \map \psi {\frac 1 3}
      | r = -2 \gamma - 3 \ln 3 - \pi \map \cot {\frac \pi 3}
      | c = adding lines $1$ and $2$
}}
{{eqn | ll= \leadsto
      | l = \map \psi {\frac 1 3}
      | r = -\gamma - \dfrac 3 2 \ln 3 - \dfrac \pi {2 \sqrt 3}
      | c = dividing by $2$ and {{cot|60}}
}}
{{end-eqn}}
{{qed}}
Theorem: Digamma Function of One Fourth

:$\map \psi {\dfrac 1 4} = -\gamma - 3 \ln 2 - \dfrac \pi 2$

Proof:
{{begin-eqn}}
{{eqn | l = \map \psi {\frac 1 4}
      | r = -\gamma - \ln 8 - \frac \pi 2 \map \cot {\frac 1 4 \pi} + 2 \sum_{n \mathop = 1}^{\ceiling {4 / 2} - 1} \map \cos {\frac {2 \pi n} 4} \map \ln {\map \sin {\frac {\pi n} 4} }
      | c = Gauss's Digamma Theorem
}}
{{eqn | r = -\gamma - 3 \ln 2 - \frac \pi 2 \times 1 + 2 \times 0 \times \map \ln {\frac {\sqrt 2} 2}
      | c = {{cot|45}}, {{cos|90}}, {{sin|45}} and Sum of Logarithms
}}
{{eqn | r = -\gamma - 3 \ln 2 - \dfrac \pi 2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Digamma Function of One Fourth

:$\map \psi {\dfrac 1 4} = -\gamma - 3 \ln 2 - \dfrac \pi 2$

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 1}^{n - 1} \map \psi {\frac k n}
      | r = -\paren {n - 1} \gamma - n \ln n
      | c = {{Corollary|Digamma Additive Formula}}
}}
{{eqn | ll= \leadsto
      | l = \sum_{k \mathop = 1}^{4 - 1} \map \psi {\frac k 4}
      | r = -\paren {4 - 1} \gamma - 4 \ln 4
      | c = 
}}
{{eqn | ll= \leadsto
      | n = 1
      | l = \map \psi {\frac 1 4} + \map \psi {\frac 2 4} + \map \psi {\frac 3 4}
      | r = -3 \gamma - 4 \ln 4
      | c = 
}}
{{eqn | n = 2
      | l = \map \psi {\frac 1 4} - \map \psi {\frac 3 4}
      | r = -\pi \map \cot {\frac \pi 4}
      | c = Digamma Reflection Formula
}}
{{eqn | ll= \leadsto
      | l = 2 \map \psi {\frac 1 4} + \map \psi {\frac 1 2}
      | r = -3 \gamma - 4 \ln 4 - \pi \map \cot {\frac \pi 4}
      | c = adding lines $1$ and $2$
}}
{{eqn | ll= \leadsto
      | l = 2 \map \psi {\frac 1 4}
      | r = -3 \gamma - 4 \ln 4 - \pi \map \cot {\frac \pi 4} - \map \psi {\frac 1 2}
      | c = subtracting $\map \psi {\frac 1 2}$ from both sides
}}
{{eqn | r = -3 \gamma - 8 \ln 2 - \pi \paren 1 - \paren {-\gamma - 2 \ln 2}
      | c = Digamma Function of One Half, Logarithm of Power and {{cot|45}}
}}
{{eqn | r = -2 \gamma - 6 \ln 2 -\pi
      | c = 
}}
{{eqn | ll = \leadsto
      | l = \map \psi {\frac 1 4}
      | r = -\gamma - 3 \ln 2 - \dfrac \pi 2
      | c = dividing by $2$
}}
{{end-eqn}}
{{qed}}
Theorem: Digamma Function of Two Thirds

:$\map \psi {\dfrac 2 3} = -\gamma - \dfrac 3 2 \ln 3 + \dfrac \pi {2 \sqrt 3}$

Proof:
{{begin-eqn}}
{{eqn | l = \map \psi {\frac 1 3} - \map \psi {\frac 2 3}
      | r = -\pi \map \cot {\frac \pi 3}
      | c = Digamma Reflection Formula
}}
{{eqn | ll= \leadsto
      | l = \map \psi {\frac 2 3}
      | r = \pi \map \cot {\frac \pi 3} + \map \psi {\frac 1 3}
      | c = rearranging 
}}
{{eqn | r = \dfrac \pi {\sqrt 3} + \paren {-\gamma - \dfrac 3 2 \ln 3 - \dfrac \pi {2 \sqrt 3} }
      | c = {{cot|60}} and Digamma Function of One Third
}}
{{eqn | r = -\gamma - \dfrac 3 2 \ln 3 + \dfrac \pi {2 \sqrt 3}
      | c = rearranging
}}
{{end-eqn}}
{{qed}}
Category:Examples of Digamma Function
Category:Euler-Mascheroni Constant
ezjstzqq3yt0wja5ywj3rdi7mizi4c8
Theorem: Digamma Function of Three Fourths

:$\map \psi {\dfrac 3 4} = -\gamma - 3 \ln 2 + \dfrac \pi 2$

Proof:
{{begin-eqn}}
{{eqn | l = \map \psi {\frac 1 4} - \map \psi {\frac 3 4}
      | r = -\pi \map \cot {\frac \pi 4}
      | c = Digamma Reflection Formula
}}
{{eqn | ll= \leadsto
      | l = \map \psi {\frac 3 4}
      | r = \pi \map \cot {\frac \pi 4} + \map \psi {\frac 1 4}
      | c = rearranging 
}}
{{eqn | r = \pi \times 1 + \paren {-\gamma - 3 \ln 2 - \dfrac \pi 2}
      | c = {{cot|45}} and Digamma Function of One Fourth
}}
{{eqn | r = -\gamma - 3 \ln 2 + \dfrac \pi 2
      | c = rearranging
}}
{{end-eqn}}
{{qed}}
Category:Examples of Digamma Function
Category:Euler-Mascheroni Constant
0wi7bnz9ljbku106qylaoyil4dznvp5
Theorem: Digamma Function of One Sixth

:$\map \psi {\dfrac 1 6} = -\gamma - 2 \ln 2 - \dfrac 3 2 \ln 3 - \dfrac {\pi \sqrt 3} 2$

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 1}^{n - 1} \map \psi {\frac k n}
      | r = -\paren {n - 1} \gamma - n \ln n
      | c = {{Corollary|Digamma Additive Formula}}
}}
{{eqn | ll= \leadsto
      | l = \sum_{k \mathop = 1}^{6 - 1} \map \psi {\frac k 6}
      | r = -\paren {6 - 1} \gamma - 6 \ln 6
      | c = 
}}
{{eqn | ll= \leadsto
      | n = 1
      | l = \map \psi {\frac 1 6} + \map \psi {\frac 2 6} + \map \psi {\frac 3 6} + \map \psi {\frac 4 6} + \map \psi {\frac 5 6}
      | r = -5 \gamma - 6 \ln 6
      | c = 
}}
{{eqn | n = 2
      | l = \map \psi {\frac 1 6} - \map \psi {\frac 5 6}
      | r = -\pi \map \cot {\frac \pi 6}
      | c = Digamma Reflection Formula
}}
{{eqn | ll= \leadsto
      | l = 2 \map \psi {\frac 1 6} + \map \psi {\frac 2 6} + \map \psi {\frac 3 6} + \map \psi {\frac 4 6}
      | r = -5 \gamma - 6 \ln 6 - \pi \map \cot {\frac \pi 6}
      | c = adding lines $1$ and $2$
}}
{{eqn | ll= \leadsto
      | l = 2 \map \psi {\frac 1 6}
      | r = -5 \gamma - 6 \ln 6 - \pi \map \cot {\frac \pi 6} - \map \psi {\frac 1 3} - \map \psi {\frac 1 2} - \map \psi {\frac 2 3}
      | c = rearranging
}}
{{eqn | r = -5 \gamma - 6 \ln 2 - 6 \ln 3 - \pi \times \sqrt 3
      | c = Sum of Logarithms, {{cot|30}},
}}
{{eqn | o = 
      | ro= -
      | r = \paren {-\gamma - \dfrac 3 2 \ln 3 - \dfrac \pi {2 \sqrt 3} }
      | c = Digamma Function of One Third,
}}
{{eqn | o = 
      | ro= -
      | r = \paren {-\gamma - 2 \ln 2}
      | c = Digamma Function of One Half,
}}
{{eqn | o = 
      | ro= -
      | r = \paren {-\gamma - \dfrac 3 2 \ln 3 + \dfrac \pi {2 \sqrt 3} }
      | c = and Digamma Function of Two Thirds
}}
{{eqn | r = -2 \gamma - 4 \ln 2  - 3 \ln 3 - \pi \sqrt 3
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \map \psi {\frac 1 6}
      | r = -\gamma - 2 \ln 2 - \dfrac 3 2 \ln 3 - \dfrac {\pi \sqrt 3} 2
      | c = dividing by $2$
}}
{{end-eqn}}
{{qed}}
Theorem: Digamma Function of Five Sixths

:$\map \psi {\dfrac 5 6} = -\gamma - 2 \ln 2  - \dfrac 3 2 \ln 3 + \dfrac {\pi \sqrt 3} 2$

Proof:
{{begin-eqn}}
{{eqn | l = \map \psi {\frac 1 6} - \map \psi {\frac 5 6}
      | r = -\pi \map \cot {\frac \pi 6}
      | c = Digamma Reflection Formula
}}
{{eqn | ll= \leadsto
      | l = \map \psi {\frac 5 6}
      | r = \pi \map \cot {\frac \pi 6} + \map \psi {\frac 1 6}
      | c = rearranging 
}}
{{eqn | r = \pi \times \sqrt 3 + \paren {-\gamma - 2 \ln 2 - \dfrac 3 2 \ln 3 - \dfrac {\pi \sqrt 3} 2}
      | c = {{cot|30}} and Digamma Function of One Sixth
}}
{{eqn | r = -\gamma - 2 \ln 2 - \dfrac 3 2 \ln 3 + \dfrac {\pi \sqrt 3} 2
      | c = rearranging
}}
{{end-eqn}}
{{qed}}
Category:Examples of Digamma Function
Category:Euler-Mascheroni Constant
sz42fkyg3k9n68r4rdloonapw7yipsu
Theorem: Digamma Reflection Formula

:$\map \psi z - \map \psi {1 - z} = -\pi \cot \pi z$

Proof:
=== Lemma ===
{{:Polygamma Reflection Formula/Lemma}}{{qed|lemma}}
{{begin-eqn}}
{{eqn | l = \map \Gamma z \map \Gamma {1 - z}
      | r = \dfrac \pi {\sin \pi z}
      | c = Euler's Reflection Formula
}}
{{eqn | ll= \leadsto
      | l = \map \ln {\map \Gamma z \map \Gamma {1 - z} }
      | r = \map \ln {\dfrac \pi {\sin \pi z} }
      | c = applying $\ln$ on both sides
}}
{{eqn | ll= \leadsto
      | l = \map \ln {\map \Gamma z} + \map \ln {\map \Gamma {1 - z} }
      | r = \ln \pi - \map \ln {\sin \pi z}
      | c = Sum of Logarithms and Difference of Logarithms
}}
{{eqn | ll= \leadsto
      | l = \dfrac \d {\d z} \map \ln {\map \Gamma z} + \dfrac \d {\d z} \map \ln {\map \Gamma {1 - z} }
      | r = \dfrac \d {\d z} \ln \pi - \dfrac \d {\d z} \map \ln {\sin \pi z}
      | c = differentiating {{WRT|Differentiation}} $z$
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\map {\Gamma'} z} {\map \Gamma z} - \dfrac {\map {\Gamma'} {1 - z} } {\map \Gamma {1 - z} }
      | r = 0 - \pi \cot \pi z
      | c = Derivative of Natural Logarithm Function, Derivative of Sine Function, Chain Rule for Derivatives, Derivative of Constant
}}
{{eqn | ll= \leadsto
      | l = \map \psi z - \map \psi {1 - z}
      | r = -\pi \cot \pi z
      | c = {{Defof|Digamma Function}}
}}
{{end-eqn}}
Finally, from the {{Lemma|Polygamma Reflection Formula}}, we note that:
:$\map \psi z - \map \psi {1 - z}$
is defined on the domain $\C \setminus \Z$.
{{qed}}
Theorem: Recurrence Relation for Digamma Function

:$\map \psi {z + 1} = \map \psi z + \dfrac 1 z$

Proof:
{{begin-eqn}}
{{eqn | l = \map \Gamma {z + 1}
	  | r = z \map \Gamma z 
      | c = Gamma Difference Equation
}}
{{eqn | ll= \leadsto
	  | l = \map \ln {\map \Gamma {z + 1} }
	  | r = \map \ln {z \map \Gamma z}
      | c = applying $\ln$ on both sides
}}
{{eqn | r = \ln z + \map \ln {\map \Gamma z}
      | c = Sum of Logarithms
}}
{{eqn | ll= \leadsto
	  | l = \dfrac \d {\d z} \map \ln {\map \Gamma {z + 1} }
	  | r = \dfrac \d {\d z} \ln z + \dfrac \d {\d z} \map \ln {\map \Gamma z}
      | c = differentiation {{WRT|Differentiation}} $z$
}}
{{eqn | ll= \leadsto
	  | l = \dfrac {\map {\Gamma'} {z + 1} } {\map \Gamma {z + 1} }
	  | r = \dfrac 1 z + \dfrac {\map {\Gamma'} z} {\map \Gamma z}
      | c = Derivative of Natural Logarithm Function, Chain Rule for Derivatives
}}
{{eqn | ll= \leadsto
	  | l = \map \psi {z + 1}
	  | r = \map \psi z + \dfrac 1 z
      | c = {{Defof|Digamma Function}}
}}
{{end-eqn}}
{{qed}}
Theorem: Lattice Homomorphism is Both Meet and Join Semilattice Homomorphism

Let $L_1 = \struct{S_1, \vee_1, \wedge_1, \preceq_1}$ and $L_2 = \struct{S_2, \vee_2, \wedge_2, \preceq_2}$ be lattices.
Let $\phi: L_1 \to L_2$ be a lattice homomorphsm between $L_1$ and $L_2$.
Then:
:* $\phi: \struct{S_1, \vee_1, \preceq_1} \to \struct{S_2, \vee_2, \preceq_2}$
:* $\phi: \struct{S_1, \wedge_1, \preceq_1} \to \struct{S_2, \wedge_2, \preceq_2}$ 
are semilattice homomorphisms

Proof:
This follows immediately from:
:* Definition:Lattice (Order Theory)
:* Definition:Semilattice
:* Definition:Lattice Homomorphism
:* Definition:Semilattice Homomorphism
{{qed}}
Category:Lattice Homomorphisms
bxj5phrwt6qbj1pyl4ltpbnuosvdew4
Theorem: Lattice Homomorphism is Order-Preserving

Let $L_1 = \struct{S_1, \vee_1, \wedge_1, \preceq_1}$ and $L_2 = \struct{S_2, \vee_2, \wedge_2, \preceq_2}$ be lattices.
Let $\phi: L_1 \to L_2$ be a lattice homomorphsm between $L_1$ and $L_2$.
Then:
:$\phi: \struct{S_1, \preceq_1} \to \struct{S_2, \preceq_2}$ is order-preserving

Proof:
From Lattice Homomorphism is Both Meet and Join Semilattice Homomorphism:
:$\phi: \struct{S_1, \vee_1, \preceq_1} \to \struct{S_2, \vee_2, \preceq_2}$ is a semilattice homomorphism
From Semilattice Homomorphism is Order-Preserving:
:$\phi: \struct{S_1, \preceq_1} \to \struct{S_2, \preceq_2}$ is order-preserving
{{qed}}
Category:Lattice Homomorphisms
700acg2chvwuyrw3czeyc6c6lnq3egj
Theorem: Ordered Set has Upper Bound iff has Greatest Element

Let $\struct{S,\preceq}$ be an ordered set.
Then:
:$S$ has an upper bound in $\struct{S,\preceq}$ {{iff}} $\struct{S,\preceq}$ has a greatest element

Proof:
This follows immediately from:
:* Definition:Upper Bound
:* Definition:Greatest Element
{{qed}}
Category:Greatest Elements
Category:Ordered Sets
57i8my33m9a21nxibyxjkmcdo4hop64
Theorem: Ordered Set has Lower Bound iff has Smallest Element

Let $\struct{S,\preceq}$ be an ordered set.
Then:
:$S$ has a lower bound in $\struct{S,\preceq}$ {{iff}} $\struct{S,\preceq}$ has a smallest element

Proof:
This follows immediately from:
:* Definition:Lower Bound
:* Definition:Smallest Element
{{qed}}
Category:Smallest Elements
Category:Ordered Sets
q89lwnug5ka01sl6xy8p7kkhkgg8qrq
Theorem: Ramanujan Phi Function in terms of Digamma Function

:$\map \psi {\dfrac 1 z} + \map \psi {1 - \dfrac 1 z} = -2 \gamma - z \map \phi z$

Proof:
{{begin-eqn}}
{{eqn | l = \map \psi {\frac 1 z} + \map \psi {1 - \frac 1 z}
      | r = -z + \map \psi {1 + \frac 1 z} + \map \psi {1 - \frac 1 z}
      | c = Recurrence Relation for Digamma Function: $\map \psi {z + 1} = \map \psi z + \dfrac 1 z$
}}
{{eqn | r = -z + \paren {-\gamma + \sum_{n \mathop = 1}^\infty \paren {\frac 1 n - \frac 1 {\paren {1 + \dfrac 1 z} + n - 1} } } + \paren {-\gamma + \sum_{n \mathop = 1}^\infty \paren {\frac 1 n - \frac 1 {\paren {1 - \dfrac 1 z} + n - 1} } }
      | c = Reciprocal times Derivative of Gamma Function: $\ds \dfrac {\map {\Gamma'} z} {\map \Gamma z} = -\gamma + \sum_{n \mathop = 1}^\infty \paren {\frac 1 n - \frac 1 {z + n - 1} }$
}}
{{eqn | r = -2 \gamma - z + \sum_{n \mathop = 1}^\infty \paren {\frac 2 n - \frac 1 {\paren {n + \dfrac 1 z} } - \frac 1 {\paren {n - \dfrac 1 z} } }
      | c = Linear Combination of Convergent Series
}}
{{eqn | r = -2 \gamma - z + \sum_{n \mathop = 1}^\infty \paren {\paren {\frac z z} \times \frac 2 n - \paren {\frac z z} \times \frac 1 {\paren {n + \dfrac 1 z} } - \paren {\frac z z} \times \frac 1 {\paren {n - \dfrac 1 z} } }
      | c = multiplying top and bottom by $z$
}}
{{eqn | r = -2 \gamma - z + \sum_{n \mathop = 1}^\infty \paren {\frac {2 z} {n z} - \frac z {\paren {n z + 1} } - \frac z {\paren {n z - 1} } }
      | c = 
}}
{{eqn | r = -2 \gamma - z + z \sum_{n \mathop = 1}^\infty \paren {\frac {2 \paren {\paren {n z}^2 - 1} - \paren {n z} \paren {n z - 1} - \paren {n z} \paren {n z + 1} } {\paren {\paren {n z}^3 - n z} }  }
      | c = Difference of Two Squares
}}
{{eqn | r = -2 \gamma - z + z \sum_{n \mathop = 1}^\infty \paren {\frac {2 n^2 z^2 - 2 - n^2 z^2 + n z - n^2 z^2 - n z} {\paren {\paren {n z}^3 - n z} }  }
      | c = 
}}
{{eqn | r = -2 \gamma - z - 2 z \sum_{n \mathop = 1}^\infty \frac 1 {\paren {\paren {n z}^3 - n z} } 
      | c = 
}}
{{eqn | r = -2 \gamma - z \paren {1 + 2 \sum_{n \mathop = 1}^\infty \frac 1 {\paren {\paren {n z}^3 - n z} } }
      | c = 
}}
{{eqn | r = -2 \gamma - z \map \phi z
      | c = {{Defof|Ramanujan Phi Function of One Argument}}
}}
{{end-eqn}}
{{qed}}
Theorem: Bounded Lattice has Both Greatest Element and Smallest Element

Let $\struct {S, \vee, \wedge, \preceq}$ be a bounded lattice.
Then:
:$(1): \quad \struct {S, \preceq}$ has a smallest element, namely:
::::$\bot := \sup \O$
:$(2): \quad \struct {S, \preceq}$ has a greatest element, namely:
::::$\top := \inf \O$

Proof:
By definition of bounded lattice:
:$\bot = \sup \O$ and $\top = \inf \O$ exist
From Supremum of Empty Set is Smallest Element:
:$\bot = \sup \O$ {{iff}} $\bot$ is the smallest element of $\struct {S, \preceq}$
From Infimum of Empty Set is Greatest Element:
:$\top = \inf \O$ {{iff}} $\top$ is the greatest element of $\struct {S, \preceq}$
{{qed}}
Category:Bounded Lattices
8rkdbv3130ugg1g0n9j6v2p96rg17qh
Theorem: Dirichlet Eta Function at Non-Positive Integers

Let $n \ge 0$ be a integer. 
Then: 
:$\map \eta {-n} = \dfrac {\paren {-1}^{n + 1} \paren {2^{n + 1 } - 1} B_{n + 1} } {n + 1}$ 
where:
:$B_n$ is the $n$th Bernoulli number
:$\eta$ is the Dirichlet eta function

Proof:
{{begin-eqn}}
{{eqn | l = \map \eta s
      | r = \paren {1 - 2^{1 - s} } \map \zeta s
      | c = Riemann Zeta Function in terms of Dirichlet Eta Function
}}
{{eqn | ll = \leadsto
      | l = \map \eta {- n}
      | r = \paren {1 - 2^{1 - \paren {-n} } } \map \zeta {-n}
      | c = setting $s := - n$
}}
{{eqn | r = \paren {1 - 2^{n + 1} } \map \zeta {-n}
      | c = 
}}
{{eqn | r = \paren {1 - 2^{n + 1} } \paren {\paren {-1}^n \dfrac {B_{n + 1} } {n + 1} }
      | c = Riemann Zeta Function at Non-Positive Integers
}}
{{eqn | r = \paren {-1} \times \paren {1 - 2^{n + 1 } } \times \paren {-1} \times \paren {\paren {-1}^n \dfrac {B_{n + 1} } {n + 1} }
      | c = multiplying by $1$: $-1 \times -1 = 1$
}}
{{eqn | r = \dfrac {\paren {-1}^{n + 1} \paren {2^{n + 1 } - 1 } B_{n + 1} } {n + 1}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Integral Form of Ramanujan Phi Function

:$\ds \map \phi x = \int_{\to 0}^{\to 1} \paren {\dfrac {u^{x - 2} \paren {1 - u}^2} {1 - u^x} } \rd u + 1$
where:
:$\map \phi x$ denotes the Ramanujan phi function
:$x \in \C$
:$\map \Re x > 1$

Proof:
{{begin-eqn}}
{{eqn | l = \int_{\to 0}^{\to 1} \paren {\frac {u^{x - 2} \paren {1 - u}^2} {1 - u^x} } \rd u + 1
      | r = 1 + \int_{\to 0}^{\to 1} \paren {\frac {u^x} {1 - u^x} } \times \paren {u^{-2} \paren {1 - 2 u + u^2} } \rd u
      | c = Square of Sum
}}
{{eqn | r = 1 + \int_{\to 0}^{\to 1} \paren {\frac {u^x} {1 - u^x} } \times \paren {\paren {u^{-2} - 2 u^{-1} + 1} } \rd u
      | c = distributing the $u^{-2}$
}}
{{eqn | r = 1 + \int_{\to 0}^{\to 1} \paren {\sum_{k \mathop = 1}^{\infty} u^{k x} } \times \paren {\paren {u^{-2} - 2 u^{-1} + 1} } \rd u
      | c = Sum of Infinite Geometric Sequence
}}
{{eqn | r = 1 + \int_{\to 0}^{\to 1} \sum_{k \mathop = 1}^{\infty} \paren {u^{k x - 2} - 2 u^{k x - 1} + u^{k x} } \rd u
      | c = Linear Combination of Integrals
}}
{{eqn | r = 1 + \sum_{k \mathop = 1}^{\infty} \int_{\to 0}^{\to 1} \paren {u^{k x - 2} - 2 u^{k x - 1} + u^{k x} } \rd u
      | c = Tonelli's Theorem
}}
{{eqn | r = 1 + \paren {\sum_{k \mathop = 1}^{\infty} \intlimits {\frac {u^{k x - 1} } {k x - 1} - 2 \frac {u^{k x} } {k x} + \frac {u^{k x + 1} } {k x + 1} } {u \mathop = 0} {u \mathop = 1} }
      | c = Integral of Power
}}
{{eqn | r = 1 + \paren {\sum_{k \mathop = 1}^{\infty} \paren {\frac {1^{k x - 1} } {k x - 1} - 2 \frac {1^{k x} } {k x} + \frac {1^{k x + 1} } {k x + 1} } - \paren {\frac {0^{k x - 1} } {k x - 1} - 2 \frac {0^{k x} } {k x} + \frac {0^{k x + 1} } {k x + 1} } }
      | c = 
}}
{{eqn | r = 1 + \paren {\sum_{k \mathop = 1}^{\infty} \dfrac 1 {k x - 1} - \dfrac 2 {k x} + \dfrac 1 {k x + 1} }
      | c = simplifying
}}
{{eqn | r = 1 + \paren {\sum_{k \mathop = 1}^{\infty} \dfrac {k x \paren {k x + 1} - 2 \paren {k x + 1} \paren {k x - 1} + k x \paren {k x - 1} } {k x \paren {k x + 1} \paren {k x - 1} } }
      | c = putting everything over a common denomninator
}}
{{eqn | r = 1 + \paren {\sum_{k \mathop = 1}^\infty \frac {\paren {k^2 x^2 + k x} - 2 \paren {k^2 x^2 - 1} + \paren {k^2 x^2 - k x} } {\paren {k x}^3 - k x} }
      | c = Difference of Two Squares and multiplying out
}}
{{eqn | r = 1 + 2 \sum_{k \mathop = 1}^\infty \frac 1 {\paren {\paren {k x}^3 - k x} }
      | c = simplifying
}}
{{eqn | r = \map \phi x
      | c = {{Defof|Ramanujan Phi Function of One Argument}}
}}
{{end-eqn}}
{{qed}}
Theorem: Complete Lattice has Both Greatest Element and Smallest Element

Let $\struct{S, \vee, \wedge, \preceq}$ be a complete lattice.
Then:
:$(\text{1}) \quad \struct{S, \preceq}$ has a smallest element, namely:
::$\quad \bot := \sup \O$
:$(\text{2}) \quad \struct{S, \preceq}$ has a greatest element, namely:
::$\quad \top := \inf \O$

Proof:
From Complete Lattice is Bounded:
:$\struct{S, \vee, \wedge, \preceq}$ is a bounded lattice
From Bounded Lattice has Both Greatest Element and Smallest Element:
:$(\text{1}) \quad \struct{S, \preceq}$ has a smallest element, namely:
::$\quad \bot := \sup \O$
:$(\text{2}) \quad \struct{S, \preceq}$ has a greatest element, namely:
::$\quad \top := \inf \O$
{{qed}}
Category:Complete Lattices
0eosxreiouwkdr9e5vzi7yrikzggdbq
Theorem: Equivalence of Complete Semilattice and Complete Lattice

Let $\struct {S, \preceq}$ be an ordered set.
{{TFAE}}:
:$(\text 1) \quad \struct {S, \preceq}$ is a complete join semilattice
:$(\text 2) \quad \struct {S, \preceq}$ is a complete meet semilattice
:$(\text 3) \quad \struct {S, \preceq}$ is a complete lattice

Proof:
=== Statement $(\text 1)$ implies Statement $(\text 2)$ ===
Let $\struct {S, \preceq}$ be a complete join semilattice.
Let $A \subseteq S$.
Let $T = \leftset{s \in S : s}$ is a lower bound for $\rightset{A}$
By definition of complete join semilattice:
:$\sup T$ exists in $\struct {S, \preceq}$
Let $a = \sup T$.
We have:
:$\forall s \in A : s$ is an upper bound for $T$
By definition of supremum:
:$\forall s \in A: a \preceq s$
By definition of lower bound:
:$a$ is a lower bound for $A$
Since $a$ is the supremum of all lower bounds of $A$:
:$a = \inf A$
Since $A$ was arbitrary:
:$\forall A \subseteq S : \inf A \in S$
Hence $\struct {S, \preceq}$ is a complete meet semilattice by definition.
{{qed|lemma}}
Theorem: Complete Join Semilattice is Dual to Complete Meet Semilattice

Let $\struct {S, \preceq}$ be an ordered set.
The following are dual statements:
:$\struct{S, \preceq}$ is a complete join semilattice
:$\struct{S, \preceq}$ is a complete meet semilattice

Proof:
By definition of complete join semilattice:
:$\struct{S, \preceq}$ is a complete join semilattice 
{{iff}}:
:$\forall S' \subseteq S : \sup S' \in S$, where $\sup S'$ is the  supremum  of $S'$
The dual of this statement is:
:$\forall S' \subseteq S : \inf S' \in S$, where $\inf S'$ is the  infimum  of $S'$ by Dual Pairs (Order Theory).
By definition of complete meet semilattice:
:$\struct{S, \preceq}$ is a complete meet semilattice 
{{qed}}
Theorem: Axes of Symmetry for Ellipse

Let $K$ be an ellipse.
Then $K$ has exactly $2$ axis of bilateral symmetry:
:the major axis of $K$
:the minor axis of $K$.

Proof:
From:
:Major Axis of Ellipse is Axis of Symmetry
:Minor Axis of Ellipse is Axis of Symmetry
we have that these diameters of $K$ are in fact axis of bilateral symmetry.
It remains to be shown that there are no more.
{{ProofWanted}}