avewright/proofwiki-math huggingface dataset:
Theorem: Volume of Cone

Let $K$ be a cone whose base is of area $A$ and whose height is $h$.
Then the volume of $K$ is given by:
:$V_K = \dfrac {A h} 3$

Proof:
Let the cone be of height $h$.
Let the area of the base of the cone be $A$.
From Volume of Cylinder in terms of Height and Base Area, the volume of a cylinder of base $A$ and height $h$ is $A h$.
Let the cone be divided by planes parallel to its base each positioned some small distance $d$ apart.
Let $d$ be sufficiently small that they can be approximated to cylinders in shape.
Let there be $n$ of these small cylinders in total.
Let the volumes of each of these small cylinders be:
:$v_1, v_2, v_3, \ldots, v_n$
starting from the base of the cone and working up.
We have that:
:$v_k = d a_k$
where $a_n$ is the 
Let the areas of the bases of each of these small cylinders be:
:$a_1, a_2, a_3, \ldots, a_n$
starting from the base of the cone and working up.
{{improve|clumsy}}
{{finish}}
Theorem: Volume of Right Circular Cylinder

The volume $V_C$ of a right circular cylinder whose bases are circles of radius $r$ and whose height is $h$ is given by the formula:
:$V_C = \pi r^2 h$

Proof:
Consider a right circular cylinder $C$ whose base is a circle of radius $r$ and whose height is $h$.
Let $V_C$ denote the volume of $C$.
From Volume of Cylinder in terms of Height and Base Area:
:$V_C = A h$
where $A$ is the area of the base of $C$.
From Area of Circle, the area of each base is:
:$A = \pi r^2$
Hence:
:$V_C = \pi r^2 h$
{{qed}}
Theorem: Volume of Right Circular Cylinder

The volume $V_C$ of a right circular cylinder whose bases are circles of radius $r$ and whose height is $h$ is given by the formula:
:$V_C = \pi r^2 h$

Proof:
:600px
Consider a right circular cylinder $C$ whose base is a circle of radius $r$ and whose height is $h$.
Consider a cuboid $K$ whose height is $h$ and whose base has the same area as the base of $C$.
Let the area of those bases be $A$.
Let $C$ be positioned with its base in the same plane as the base of $K$.
By Cavalieri's Principle $C$ and $K$ have the same volume.
The bases of $C$ are circles of radius $r$.
From Area of Circle, the area of each base therefore gives:
:$A = \pi r^2$
From Volume of Cuboid, $K$ has volume given by:
:$V_K = A h = \pi r^2 h$
Hence the result.
{{qed}}
Theorem: Slope of Tangent to Cycloid

Let $C$ be a cycloid generated by the equations:
:$x = a \paren {\theta - \sin \theta}$
:$y = a \paren {1 - \cos \theta}$
The slope of the tangent to $C$ at the point $\tuple {x, y}$ is given by:
:$\dfrac {\d y} {\d x} = \cot \dfrac \theta 2$

Proof:
By Derivative of Curve at Point, the tangent to $C$ at the point $\tuple {x, y}$ is the derivative of its equation at that point.
Thus:
{{begin-eqn}}
{{eqn | l = \frac {\d x} {\d \theta}
      | r = a \paren {1 - \cos \theta}
      | c = 
}}
{{eqn | l = \frac {\d y} {\d \theta}
      | r = a \sin \theta
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d y} {\d x}
      | r = \frac {\d y} {\d \theta} / \frac {\d x} {\d \theta}
      | c = 
}}
{{eqn | r = \frac {a \sin \theta} {a \paren {1 - \cos \theta} }
      | c = 
}}
{{eqn | r = \frac {\sin \theta} {1 - \cos \theta}
      | c = 
}}
{{eqn | r = \frac 1 {\map \tan {\theta / 2} }
      | c = {{Corollary|Half Angle Formula for Tangent|2}}
}}
{{eqn | r = \cot \frac \theta 2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Slope of Tangent to Cycloid

Let $C$ be a cycloid generated by the equations:
:$x = a \paren {\theta - \sin \theta}$
:$y = a \paren {1 - \cos \theta}$
The slope of the tangent to $C$ at the point $\tuple {x, y}$ is given by:
:$\dfrac {\d y} {\d x} = \cot \dfrac \theta 2$

Proof:
Consider a polygon $ABCD$ being rolled along a straight line in the same way as the generating circle of $C$.
Let $A', B', C', D'$ be the points around which the $ABCD$ rotates while rolling.
:600px
The point $A$ traces out in succession several arcs of circles with centers $B', C', D'$.
The tangent to each of these arcs is perpendicular to the line joining the point of tangency to the corresponding point of rotation.
Consider a circle as being a polygon with an infinite number of sides.
It follows that in the limit the tangent to $C$ at any given point is perpendicular to the line joining the point of tangency to the corresponding point where the generating circle touches the straight line along which the generating circle rolls.
:600px
Let $O$ be the center of the generating circle.
Let $P$ be the point of tangency.
Let $Q$ be the point where the generating circle touches the straight line along which the generating circle rolls.
Let $S$ be the point where the tangent to $C$ meets the straight line along which the generating circle rolls.
As $OP$ and $OQ$ are both radii of the generating circle:
:$OP = OQ = a$
and so $\triangle POQ$ is isosceles.
Let $R$ be dropped perpendicular to $PQ$ at $R$.
As $\triangle POQ$ is isosceles, $\triangle OPR = \triangle OQR$ and so $PR = RQ$.
Thus $\angle POR = \angle QOR = \dfrac \theta 2$.
As $OR \perp PR$ and $PR \perp PS$, we have that $\triangle OPR$ is similar to $\triangle QPS$.
Thus $\angle PQS = \angle POR$ and so $\angle PSQ$ is $\dfrac \pi 2 - \angle POR = \dfrac \pi 2 - \dfrac \theta 2$.
By definition, $\tan \angle PSQ$ is the slope of the tangent $\dfrac {\d y} {\d x}$ to $C$.
Thus:
{{begin-eqn}}
{{eqn | l = \dfrac {\d y} {\d x}
      | r = \tan \angle PSQ
      | c = 
}}
{{eqn | r = \map \tan {\dfrac \pi 2 - \dfrac \theta 2}
      | c = 
}}
{{eqn | r = \cot \frac \theta 2
      | c = Tangent of Complement equals Cotangent
}}
{{end-eqn}}
{{qed}}
Theorem: Upper Closure of Singleton

Let $\struct {S, \preceq}$ be an ordered set.
Let $s$ be an element of $S$.
Then:
:$\set s^\succeq = s^\succeq$
where:
:$\set s^\succeq$ denotes the upper closure of $\set s$
:$s^\succeq$ denotes the upper closure of $s$

Proof:
{{begin-eqn}}
{{eqn | l = \set s^\succeq
      | r = \bigcup \set {t^\succeq: t \in \set s}
      | c = {{Defof|Upper Closure of Subset}}
}}
{{eqn | r = \bigcup \set {s^\succeq}
      | c = {{Defof|Singleton}}
}}
{{eqn | r = s^\succeq
      | c = Union of Singleton
}}
{{end-eqn}}
{{qed}}
Theorem: Lower Closure of Singleton

Let $\struct {S, \preceq}$ be an ordered set.
Let $s$ be an element of $S$.
Then:
:$\set s^\preceq = s^\preceq$
where:
:$\set s^\preceq$ denotes the lower closure of $\set s$
:$s^\preceq$ denotes the lower closure of $s$.

Proof:
{{begin-eqn}}
{{eqn | l = \set s^\preceq
      | r = \bigcup \set {t^\preceq: t \in \set s}
      | c = {{Defof|Lower Closure of Subset}}
}}
{{eqn | r = \bigcup \set {s^\preceq}
      | c = {{Defof|Singleton}}
}}
{{eqn | r = s^\preceq
      | c = Union of Singleton
}}
{{end-eqn}}
{{qed}}
Theorem: Upper Closure of Element is Filter

Let $\struct {S, \preceq}$ be an ordered set.
Let $s$ be an element of $S$.
Then:
:$s^\succeq$ is a filter in $\struct {S, \preceq}$
where $s^\succeq$ denotes the upper closure of $s$.

Proof:
By Singleton is Directed and Filtered Subset
:$\set s$ is a filtered subset of $S$
By Filtered iff Upper Closure Filtered:
:$\set s^\succeq$ is a filtered subset of $S$
By Upper Closure is Upper Section:
:$\set s^\succeq$ is a upper section in $S$
By Upper Closure of Singleton
:$\set s^\succeq = s^\succeq$
By definition of reflexivity:
:$s \preceq s$
By definition of upper closure of element:
:$s \in s^\succeq$
Thus by definition:
:$s^\succeq$ is non-empty, filtered and upper.
Thus by definition:
:$s^\succeq$ is a filter in $\struct {S, \preceq}$
{{qed}}
Theorem: Length of Logarithmic Spiral

Consider a logarithmic spiral $S$ given by the equation:
:$r = a e^{b \theta}$
Construct a tangent to $S$ at the point $Q = \tuple {a, 0}$.
Let the tangent cross the $y$-axis at $P$.
Then the length of $PQ$ equals the total length of $S$ from $P$ inwards to the origin.

Proof:
&nbsp;
:400px
{{ProofWanted}}
Theorem: Logarithmic Spiral is Equiangular

The logarithmic spiral is '''equiangular''', in the following sense:
Let $P = \polar {r, \theta}$ be a point on a logarithmic spiral $S$ expressed in polar coordinates as:
:$r = a e^{b \theta}$
Then the angle $\psi$ that the tangent makes to the radius vector of $S$ is constant and equal to $\arccot b$.

Proof:
Consider the logarithmic spiral $S$ expressed as:
:$r = a e^{b \theta}$
:400px
Let $\psi$ be the angle between the tangent to $S$ and the radius vector.
The  derivative of $r$ {{WRT|Differentiation}} $\theta$ is:
:$\dfrac {\d r} {\d \theta} = a b e^{b \theta} = b r$
and thus:
{{begin-eqn}}
{{eqn | l = \tan \psi
      | r = \frac r {\frac {\d r} {\d \theta} }
      | c = 
}}
{{eqn | r = \frac r {b r}
      | c = 
}}
{{eqn | r = \frac 1 b
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \cot \psi
      | r = b
      | c = 
}}
{{end-eqn}}
Thus for a given logarithmic spiral, $\psi$ is constant and equal to $\arccot b$.
{{qed}}
Theorem: Infimum of Upper Closure of Element

Let $\struct {S, \preceq}$ be an ordered set.
Let $s$ be an element of $S$.
Then:
:$\map \inf {s^\succeq} = s$
where $s^\succeq$ denotes the upper closure of $s$.

Proof:
{{begin-eqn}}
{{eqn | l = \map \inf {s^\succeq}
      | r = \map \inf {\set s^\succeq}
      | c = Upper Closure of Singleton
}}
{{eqn | r = \map \inf {\set s}
      | c = Infimum of Upper Closure of Set
}}
{{eqn | r = s
      | c = Infimum of Singleton
}}
{{end-eqn}}
{{qed}}
Theorem: Volume of Gabriel's Horn

Consider Gabriel's horn, the solid of revolution formed by rotating about the $x$-axis the curve:
:$y = \dfrac 1 x$
Consider the volume $V$ of the space enclosed by the planes $x = 1$, $x = a$ and the portion of Gabriel's horn where $1 \le x \le a$.
Then:
:$V = \pi \paren {1 - \dfrac 1 a}$

Proof:
From Volume of Solid of Revolution:
{{begin-eqn}}
{{eqn | l = V
      | r = \pi \int_1^a \frac 1 {x^2} \rd x
      | c =
}}
{{eqn | r = \pi \intlimits {-\dfrac 1 x} 1 a
      | c = Primitive of Power
}}
{{eqn | r = \pi \intlimits {\dfrac 1 x} a 1
      | c =
}}
{{eqn | r = \pi \paren {1 - \dfrac 1 a}
      | c =
}}
{{end-eqn}}
{{qed}}
Theorem: Pascal's Theorem

Let $ABCDEF$ be a hexagon whose $6$ vertices lie on a conic section and whose opposite sides are not parallel.
Then the points of intersection of the opposite sides, when produced as necessary, all lie on a straight line.

Proof:
:400px
:500px
{{ProofWanted}}
Theorem: Lower Closure of Element is Ideal

Let $\struct {S, \preceq}$ ne an ordered set.
Let $s$ be an element of $S$.
Then $s^\preceq$ is ideal in $\struct {S, \preceq}$
where $s^\preceq$ denotes the lower closure of $s$.

Proof:
By Singleton is Directed and Filtered Subset:
:$\set s$ is a directed subset of $S$
By Directed iff Lower Closure Directed:
:$\set s^\preceq$ is a directed subset of $S$
By Lower Closure is Lower Section:
:$\set s^\preceq$ is a lower section in $S$
By Lower Closure of Singleton
:$\set s^\preceq = s^\preceq$
By definition of reflexivity:
:$s \preceq s$
By definition of lower closure of element:
:$s \in s^\preceq$
Thus by definition:
:$s^\succeq$ is non-empty, directed and lower.
Thus by definition:
:$s^\preceq$ is a ideal in $\struct {S, \preceq}$
{{qed}}
Theorem: Supremum of Lower Closure of Element

Let $\struct {S, \preceq}$ be an ordered set.
Let $s$ be an element of $S$.
Then:
:$\map \sup {s^\preceq} = s$
where $s^\preceq$ denotes the lower closure of $s$.

Proof:
{{begin-eqn}}
{{eqn | l = \map \sup {s^\preceq}
      | r = \map \sup {\set s^\preceq}
      | c = Lower Closure of Singleton
}}
{{eqn | r = \map \sup {\set s}
      | c = Supremum of Lower Closure of Set
}}
{{eqn | r = s
      | c = Supremum of Singleton
}}
{{end-eqn}}
{{qed}}
Theorem: Upper Closure is Decreasing

Let $\struct {S, \preceq}$ be an ordered set.
Let $x, y$ be elements of $S$ such that
:$x \preceq y$
then $y^\succeq \subseteq x^\succeq$
where $y^\succeq$ denotes the upper closure of $y$.

Proof:
Let $z \in y^\succeq$.
By definition of upper closure of element:
:$y \preceq z$
By definition of ordering, $\preceq$ is transitive.
From $x \preceq y$ and $y \preceq z$:
:$x \preceq z$
Thus again by definition of upper closure of element:
:$z \in x^\succeq$
{{qed}}
Theorem: Lower Closure is Increasing

Let $\struct {S, \preceq}$ be an ordered set.
Let $x, y$ be elements of $S$ such that
:$x \preceq y$
Then:
:$x^\preceq \subseteq y^\preceq$
where $y^\preceq$ denotes the lower closure of $y$.

Proof:
Let $z \in x^\preceq$.
By definition of lower closure of element:
:$z \preceq x$
By definition of transitivity:
:$z \preceq y$
Thus again by definition of lower closure of element:
:$z \in y^\preceq$
{{qed}}
Theorem: Suprema Preserving Mapping on Ideals is Increasing

Let $\struct {S, \preceq}$ and $\struct {T, \precsim}$ be ordered sets.
Let $f: S \to T$ be a mapping.
For every ideal $I$ in $\struct {S, \preceq}$, let $f$ preserve the supremum on $I$.
Then $f$ is increasing.

Proof:
Let $x, y \in S$ such that:
:$x \preceq y$
By Supremum of Singleton:
:$\set x$ and $\set y$ admit suprema in $\struct {S, \preceq}$
By Supremum of Lower Closure of Set:
:$\set x^\preceq$ and $\set y^\preceq$ admit suprema in $\struct {S, \preceq}$
where $\set x^\preceq$ denotes the lower closure of $\set x$
By Lower Closure of Singleton:
:$x^\preceq$ and $y^\preceq$ admit suprema in $\struct {S, \preceq}$
By Lower Closure of Element is Ideal:
:$x^\preceq$ and $y^\preceq$ are ideals in $\struct {S, \preceq}$
By assumption and definition of mapping preserves the supremum on subset:
:$\map {f^\to} {x^\preceq}$ and $\map {f^\to} {y^\preceq}$ admit suprema in $\struct {T, \precsim}$
and:
:$\map \sup {\map {f^\to} {x^\preceq} } = \map f {\map \sup {x^\preceq} }$
and:
:$\map \sup {\map {f^\to} {y^\preceq} } = \map f {\map \sup {y^\preceq} }$
By Supremum of Lower Closure of Element:
:$\map \sup {x^\preceq} = x$ and $\map \sup {y^\preceq} = y$
By Lower Closure is Increasing:
:$x^\preceq \subseteq y^\preceq$
By Image of Subset under Mapping is Subset of Image:
:$\map {f^\to} {x^\preceq} \subseteq \map {f^\to} {y^\preceq}$
Thus by Supremum of Subset:
:$\map f x \precsim \map f y$
Thus by definition:
:$f$ is increasing.
{{qed}}
Theorem: Imaginary Unit to Power of Itself

:$i^i = e^{-\pi / 2}$
where $i$ is the imaginary unit.

Proof:
{{begin-eqn}}
{{eqn | l = i^i
      | r = \paren {e^{i \pi / 2} }^i
      | c = Euler's Formula
}}
{{eqn | r = e^{\pi i^2 / 2}
      | c = 
}}
{{eqn | r = e^{-\pi / 2}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Imaginary Unit to Power of Itself/Complete

:$i^i = \set {\exp \paren {\dfrac {4 k + 3} 2 \pi}: k \in \Z}$
where $i$ is the imaginary unit.

Proof:
{{begin-eqn}}
{{eqn | l = i^i
      | r = \exp \paren {i \ln \paren i}
      | c = {{Defof|Complex Power}}
}}
{{eqn | r = \exp \paren {i \paren {\ln 1 + i \paren {\dfrac \pi 2 + 2 k \pi} } }
      | c = {{Defof|Complex Natural Logarithm}}: for all $k \in \Z$
}}
{{eqn | r = \exp \paren {i \paren {i \paren {\dfrac \pi 2 + 2 k \pi} } } 
      | c = Logarithm of 1 is 0
}}
{{eqn | r = \exp \paren {i^2 \dfrac \pi 2 + 2 k \pi i^2}
      | c = 
}}
{{eqn | r = \exp \paren {-\dfrac \pi 2 - 2 k \pi}
      | c = 
}}
{{eqn | r = \exp \paren {\dfrac {3 \pi} 2 + 2 k \pi}
      | c = as $k$ ranges over all integers
}}
{{eqn | r = \exp \paren {\dfrac {4 k + 3} 2 \pi}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Riemann Zeta Function of 4

The Riemann zeta function of $4$ is given by:
{{begin-eqn}}
{{eqn | l = \map \zeta 4
      | r = \dfrac 1 {1^4} +  \dfrac 1 {2^4} +  \dfrac 1 {3^4} +  \dfrac 1 {4^4} + \cdots
      | c = 
}}
{{eqn | r = \dfrac {\pi^4} {90}
      | c = 
}}
{{eqn | o = \approx
      | r = 1 \cdotp 08232 \, 3 \ldots
      | c = 
}}
{{end-eqn}}

Proof:
By Fourier Series of Fourth Power of x, for $x \in \closedint {-\pi} \pi$:
:$\ds x^4 = \frac {\pi^4} 5 + \sum_{n \mathop = 1}^\infty \frac {8 n^2 \pi^2 - 48} {n^4} \map \cos {n \pi} \map \cos {n x}$
Setting $x = \pi$: 
{{begin-eqn}}
{{eqn | l = \pi^4 
      | r = \frac {\pi^4} 5 + \sum_{n \mathop = 1}^\infty \frac {8 n^2 \pi^2 - 48} {n^4} \map {\cos^2} {n \pi}
}}
{{eqn | ll= \leadsto
      | l = \frac {4 \pi^4} 5 
      | r = \sum_{n \mathop = 1}^\infty \frac {8 n^2 \pi^2} {n^4} - \sum_{n \mathop = 1}^\infty \frac {48} {n^4}
      | c = Cosine of Multiple of Pi
}}
{{eqn | ll= \leadsto
      | l = \frac {\pi^4} 5
      | r = 2 \pi^2 \sum_{n \mathop = 1}^\infty \frac 1 {n^2} - 12 \sum_{n \mathop = 1}^\infty \frac 1 {n^4}
}}
{{eqn | r = \frac {\pi^4} 3 - 12 \sum_{n \mathop = 1}^\infty \frac 1 {n^4}
      | c = Basel Problem
}}
{{eqn | ll= \leadsto
      | l = 12 \sum_{n \mathop = 1}^\infty \frac 1 {n^4} 
      | r = \frac {\pi^4} 3 - \frac {\pi^4} 5
      | c = rearranging
}}
{{eqn | r = \frac {2 \pi^4} {15}
}}
{{eqn | ll= \leadsto
      | l = \sum_{n \mathop = 1}^\infty \frac 1 {n^4}
      | r = \frac {\pi^4} {90}
}}
{{end-eqn}}
{{qed}}
Theorem: Riemann Zeta Function of 4

The Riemann zeta function of $4$ is given by:
{{begin-eqn}}
{{eqn | l = \map \zeta 4
      | r = \dfrac 1 {1^4} +  \dfrac 1 {2^4} +  \dfrac 1 {3^4} +  \dfrac 1 {4^4} + \cdots
      | c = 
}}
{{eqn | r = \dfrac {\pi^4} {90}
      | c = 
}}
{{eqn | o = \approx
      | r = 1 \cdotp 08232 \, 3 \ldots
      | c = 
}}
{{end-eqn}}

Proof:
By Fourier Series of x squared, for $x \in \closedint {-\pi} \pi$:
:$\ds x^2 = \frac {\pi^2} 3 + \sum_{n \mathop = 1}^\infty \paren {\paren {-1}^n \frac 4 {n^2} \cos n x}$
Hence:
{{begin-eqn}}
{{eqn | l = \frac 1 \pi \int_{-\pi}^\pi x^4 \rd x
      | r = \frac 1 2 \paren {\frac {2 \pi^2} 3}^2 + \sum_{n \mathop = 1}^\infty \paren {\frac {4 \paren {-1}^n} {n^2} }^2
      | c = Parseval's Theorem
}}
{{eqn | ll= \leadsto
      | l = \frac 2 \pi \int_0^\pi x^4 \rd x 
      | r = \frac {2 \pi^4} 9 + \sum_{n \mathop = 1}^\infty \frac {16} {n^4} 
      | c = Definite Integral of Even Function 
}}
{{eqn | ll= \leadsto
      | l = \frac {2 \pi^4} 5 
      | r = \frac {2 \pi^4} 9 + \sum_{n \mathop = 1}^\infty \frac {16} {n^4} 
}}
{{eqn | ll= \leadsto
      | l = \frac {8 \pi^4} {45} 
      | r = \sum_{n \mathop = 1}^\infty \frac {16} {n^4}
}}
{{eqn | ll= \leadsto
      | l = \sum_{n \mathop = 1}^\infty \frac 1 {n^4} 
      | r = \frac {\pi^4} {90}
}}
{{end-eqn}}
{{qed}}
Theorem: Riemann Zeta Function of 4

The Riemann zeta function of $4$ is given by:
{{begin-eqn}}
{{eqn | l = \map \zeta 4
      | r = \dfrac 1 {1^4} +  \dfrac 1 {2^4} +  \dfrac 1 {3^4} +  \dfrac 1 {4^4} + \cdots
      | c = 
}}
{{eqn | r = \dfrac {\pi^4} {90}
      | c = 
}}
{{eqn | o = \approx
      | r = 1 \cdotp 08232 \, 3 \ldots
      | c = 
}}
{{end-eqn}}

Proof:
{{ProofWanted|$\ds \int_0^1\int_0^1\int_0^1\int_0^1 \frac 1 {1 - x_1x_2x_3x_4} \rd x_1 \rd x_2 \rd x_3 \rd x_4$. Use Beukers-Calabi-Kolk sub.}}
Theorem: Riemann Zeta Function of 4

The Riemann zeta function of $4$ is given by:
{{begin-eqn}}
{{eqn | l = \map \zeta 4
      | r = \dfrac 1 {1^4} +  \dfrac 1 {2^4} +  \dfrac 1 {3^4} +  \dfrac 1 {4^4} + \cdots
      | c = 
}}
{{eqn | r = \dfrac {\pi^4} {90}
      | c = 
}}
{{eqn | o = \approx
      | r = 1 \cdotp 08232 \, 3 \ldots
      | c = 
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = \map \zeta 4
      | r = \paren {-1}^3 \dfrac {B_4 2^3 \pi^4} {4!}
      | c = Riemann Zeta Function at Even Integers
}}
{{eqn | r = \paren {-1}^3 \paren {-\dfrac 1 {30} } \dfrac {2^3 \pi^4} {4!}
      | c = {{Defof|Sequence of Bernoulli Numbers}}
}}
{{eqn | r = \paren {\dfrac 1 {30} } \paren {\dfrac 8 {24} } \pi^4
      | c = {{Defof|Factorial}}
}}
{{eqn | r = \dfrac {\pi^4} {90}
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Riemann Zeta Function of 6

The Riemann zeta function of $6$ is given by:
{{begin-eqn}}
{{eqn | l = \map \zeta 6
      | r = \dfrac 1 {1^6} +  \dfrac 1 {2^6} +  \dfrac 1 {3^6} +  \dfrac 1 {4^6} + \cdots
      | c = 
}}
{{eqn | r = \dfrac {\pi^6} {945}
      | c = 
}}
{{eqn | o = \approx
      | r = 1 \cdotp 01734 \, 3 \ldots
      | c = 
}}
{{end-eqn}}

Proof:
By Fourier Series: $x^6$ over $-\pi$ to $\pi$, for $x \in \closedint {-\pi} \pi$:
:$\ds x^6 = \frac {\pi^6} 7 + \sum_{n \mathop = 1}^\infty \frac {12 n^4 \pi^4 - 240 n^2 \pi^2 +1440} {n^6} \, \map \cos {n \pi} \, \map \cos {n x}$
Setting $x = \pi$: 
{{begin-eqn}}
{{eqn | l = \pi^6 
      | r = \frac {\pi^6} 7 + \sum_{n \mathop = 1}^\infty \frac {12 n^4 \pi^4 - 240 n^2 \pi^2 +1440} {n^6} \, \map {\cos^2} {n \pi}
}}
{{eqn | ll= \leadsto
      | l = \frac { 6 \pi^6} 7 
      | r = \sum_{n \mathop = 1}^\infty \frac {12 \pi^4} {n^2} - \sum_{n \mathop = 1}^\infty \frac {240 \pi^2} {n^4} + \sum_{n \mathop = 1}^\infty \frac {1440} {n^6}
      | c = Cosine of Multiple of Pi
}}
{{eqn | ll= \leadsto
      | l = \frac {\pi^6} 7
      | r = 2 \pi^4 \sum_{n \mathop = 1}^\infty \frac 1 {n^2} - 40 \pi^2 \sum_{n \mathop = 1}^\infty \frac 1 {n^4} + 240 \sum_{n \mathop = 1}^\infty \frac 1 {n^6}
}}
{{eqn | r = - \frac {\pi^6} 9 + 240 \sum_{n \mathop = 1}^\infty \frac 1 {n^6}
      | c = Basel Problem and Riemann Zeta Function of 4
}}
{{eqn | ll= \leadsto
      | l = 240 \sum_{n \mathop = 1}^\infty \frac 1 {n^6} 
      | r = \frac {\pi^6} 9 + \frac {\pi^6} 7
      | c = rearranging
}}
{{eqn | r = \frac {16 \pi^4} {63}
}}
{{eqn | ll= \leadsto
      | l = \sum_{n \mathop = 1}^\infty \frac 1 {n^6}
      | r = \frac {\pi^6} {945}
}}
{{end-eqn}}
{{qed}}
Theorem: Infima Preserving Mapping on Filters Preserves Filtered Infima

Let $\struct {S, \preceq}$, $\struct {T, \precsim}$ be ordered sets.
Let $f: S \to T$ be a mapping.
For every filter $F$ in $\struct {S, \preceq}$, let $f$ preserve the infimum on $F$.
Then $f$ preserves filtered infima.

Proof:
Let $F$ be a filtered subset of $S$ such that:
:$F$ admits an infimum in $\struct {S, \preceq}$.
By Filtered iff Upper Closure Filtered:
:$F^\succeq$ is filtered
where $F^\succeq$ denotes the upper closure of $F$.
By Upper Closure is Upper Section:
:$F^\succeq$ is upper.
Because filtered is non-empty, by definition:
:$F^\succeq$ is filter in $\struct {S, \preceq}$.
By Infimum of Upper Closure of Set:
:$F^\succeq$ admits an infimum in $\struct {S, \preceq}$
and
:$\map \inf {F^\succeq} = \inf F$
By assumption and mapping preserves the infimum on subset:
:$\map {f^\to} {F^\succeq}$ admits an infimum in $\struct {T, \precsim}$
and
:$\map \inf {\map {f^\to} {F^\succeq} } = \map f {\map \inf {F^\succeq} }$
By Upper Closure is Closure Operator:
:$F \subseteq F^\succeq$
By Image of Subset under Mapping is Subset of Image:
:$\map {f^\to} F \subseteq \map {f^\to} {F^\succeq}$
By definition of infimum:
:$\map f {\inf F}$ is lower bound for $\map {f^\to} {F^\succeq}$
By Lower Bound is Lower Bound for Subset:
:$\map f {\inf F}$ is a lower bound for $\map {f^\to} F$
We will prove that:
:for every element $x$ of $T$:
::if $x$ is lower bound for $\map {f^\to} F$, then $x \precsim \map f {\inf F}$
Let $x \in T$ such that:
:$x$ is a lower bound for $\map {f^\to} \F$
We will prove as a sublemma that:
:$x$ is a lower bound for $\map {f^\to} {F^\succeq}$
Let $y \in \map {f^\to} {F^\succeq}$.
By definition of image of set under mapping:
:$\exists a \in S: a \in F^\succeq \land y = \map f a$
By definition of upper closure of set:
:$\exists b \in F: b \preceq a$
By Infima Preserving Mapping on Filters is Increasing:
:$f$ is increasing.
By definition of increasing:
:$\map f b \precsim \map f a$
By definition of image of set under mapping:
:$\map f b \in \map {f^\to} F$
By definition of lower bound of set:
:$x \precsim \map f b$
Thus by definition of transitivity:
:$x \precsim y$
Thus by definition:
:$x$ is a lower bound for $\map {f^\to} {F^\succeq}$
This ends the proof of the sublemma.
Thus by definition of infimum:
:$x \precsim \map f {\inf F}$
Thus again by definition of infimum:
:$\map {f^\to} F$ admits an infimum in $\struct {T, \precsim}$
and
:$\map \inf {\map {f^\to} F} = \map f {\inf F}$
Thus result follows by definition of mapping preserves filtered infima.
{{qed}}