avewright/proofwiki-math huggingface dataset:
Theorem: Dirichlet Beta Function at Odd Positive Integers/Examples/Dirichlet Beta Function of 3

:$\map \beta 3 = \dfrac {\pi^3} {32} $

Proof:
{{begin-eqn}}
{{eqn | l = \map \beta {2 n + 1}
      | r = \paren {-1}^n \dfrac {E_{2 n} \pi^{2 n + 1} } {4^{n + 1} \paren {2 n}!}
      | c = Dirichlet Beta Function at Odd Positive Integers
}}
{{eqn | ll = \leadsto
      | l = \map \beta 3
      | r = \paren {-1}^1 \dfrac {E_2 \pi^3 } {4^2 \paren {2}!}
      | c = setting $n := 1$
}}
{{eqn | r = \frac {\pi^3} {32}
      | c = Euler Number Values: $E_2 = -1$
}}
{{end-eqn}}
{{qed}}
Category:Dirichlet Beta Function at Odd Positive Integers
Category:Examples of Dirichlet Beta Function Values
fjsbhzpcqonv0b9u4ypprlddno3rmnc
Theorem: Eccentricity of Ellipse is Linear Eccentricity over Semimajor Axis

Let $K$ be a ellipse such that:
:$a$ denotes the length of semimajor axis of $K$
:$c$ denotes the linear eccentricity of $K$
:$e$ denotes the eccentricity of $K$.
Then:
:$e = \dfrac c a$

Proof:
{{Recall|Focus-Directrix Property of Ellipse|focus-directrix property of ellipse}}
{{:Definition:Focus-Directrix Property of Ellipse}}
{{ProofWanted|straightforward but I no longer have the patience}}
Theorem: Eccentricity of Ellipse in terms of Semimajor and Semiminor Axes

Let $K$ be a ellipse such that:
:$a$ denotes the length of the semimajor axis of $K$
:$b$ denotes the length of the semiminor axis of $K$
:$e$ denotes the eccentricity of $K$.
Then:
:$e^2 = 1 - \dfrac {b^2} {a^2}$

Proof:
Let $c$ denote the linear eccentricity of $K$.
{{begin-eqn}}
{{eqn | l = a^2
      | r = b^2 + c^2
      | c = Linear Eccentricity of Ellipse from Major and Minor Axis
}}
{{eqn | ll = \leadsto
      | l = c^2
      | r = a^2 - b^2
}}
{{eqn | l = e
      | r = \frac c a
      | c = Eccentricity of Ellipse is Linear Eccentricity over Semimajor Axis
}}
{{eqn | l = e^2
      | r = \frac {c^2} {a^2}
}}
{{eqn | l = 
      | r = \frac {a^2 - b^2} {a^2}
}}
{{eqn | l =
      | r = 1 - \frac {b^2} {a^2}
}}
{{end-eqn}}
{{qed}}
Theorem: Axes of Symmetry for Ellipsoid

Let $\EE$ be an ellipsoid.
Then $\EE$ has exactly $3$ axes of symmetry:
:the major axis of $\EE$
:the mean axis of $\EE$
:the minor axis of $\EE$.

Proof:
From:
:Major Axis of Ellipsoid is Axis of Symmetry
:Mean Axis of Ellipsoid is Axis of Symmetry
:Minor Axis of Ellipsoid is Axis of Symmetry
we have that these diameters of $\EE$ are in fact axes of symmetry.
It remains to be shown that there are no more.
{{ProofWanted}}
Theorem: Minor Axis of Ellipsoid is Axis of Symmetry

Let $\EE$ be an ellipsoid.
The minor axis of $\EE$ is an axis of symmetry of $\EE$.

Proof:
Let us arrange $\EE$ such that the minor axis is aligned with the $x$-axis, say.
By Standard Equation of Ellipsoid, $\EE$ can be expressed by the equation:
:$\dfrac {x^2} {a^2} + \dfrac {y^2} {b^2} + \dfrac {z^2} {c^2} = 1$
where $2 a$ is the length of the minor axis.
Let $R$ denote the space rotation of $180 \degrees$ about the $x$-axis, that is, the minor axis of $\EE$.
Then:
{{begin-eqn}}
{{eqn | r = \map R {\dfrac {x^2} {a^2} + \dfrac {y^2} {b^2} + \dfrac {z^2} {c^2} }
      | o = 
      | c = 
}}
{{eqn | r = \dfrac {x^2} {a^2} + \dfrac {\paren {-y}^2} {b^2} + \dfrac {\paren {-z}^2} {c^2}
      | c = Space Rotation through Straight Angle about X-Axis
}}
{{eqn | r = \dfrac {x^2} {a^2} + \dfrac {y^2} {b^2} + \dfrac {z^2} {c^2}
      | c = 
}}
{{end-eqn}}
Hence $R$ is demonstrated to be a symmetry, and the result follows.
{{qed}}
Theorem: General Harmonic Numbers in terms of Riemann Zeta and Hurwitz Zeta Functions

:$\harm r x = \map \zeta r - \map \zeta {r, x + 1}$

Proof:
{{begin-eqn}}
{{eqn 	| l = \harm r x
	    | r = \sum_{k \mathop = 1}^\infty \paren {\frac 1 {k^r} - \frac 1 {\paren {k + x}^r} }
	    | c = {{Defof|General Harmonic Numbers}}
}}
{{eqn 	| r = \sum_{k \mathop = 1}^\infty \frac 1 {k^r} - \sum_{k \mathop = 1}^{\infty} \frac 1 {\paren {k + x}^r}
	    | c = 
}}
{{eqn 	| r = \sum_{k \mathop = 1}^\infty \frac 1 {k^r} - \sum_{k \mathop = 0}^{\infty} \frac 1 {\paren {k + \paren {x + 1} }^r}
	    | c = reindexing the sum
}}
{{eqn 	| r = \map \zeta r - \map \zeta {r, x + 1}
	    | c = {{Defof|Hurwitz Zeta Function}} and {{Defof|Riemann Zeta Function}}
}}
{{end-eqn}}
{{qed}}
Theorem: Plane Section of Spheroid Perpendicular to Axis of Revolution is Circle

Let $\SS$ be a spheroid.
Let $\PP$ be a plane section of $\SS$ such that $\PP$ is perpendicular to the axis of revolution of $\SS$.
Then $\PP$ is a circle.

Proof:
A spheroid is defined as the solid of revolution formed by rotation of an ellipse about one of its axes.
Hence the result by definition of solid of revolution.
{{qed}}
Theorem: Sum of General Harmonic Numbers in terms of Riemann Zeta Function

:$\ds \harm r x - \dfrac 1 {n^r} \sum_{k \mathop = 0}^{n - 1} \harm r {x - \dfrac k n} = \paren {1 - n^{1 - r} } \map \zeta r$

Proof:
=== Lemma ===
{{:Sum of General Harmonic Numbers in terms of Riemann Zeta Function/Lemma}}{{qed|lemma}}
{{begin-eqn}}
{{eqn | l = \harm r x - \dfrac 1 {n^r} \sum_{k \mathop = 0}^{n - 1} \harm r {x - \dfrac k n}
      | r = \sum_{j \mathop = 1}^\infty \paren {\frac 1 {j^r} - \frac 1 {\paren {j + x}^r} } - \dfrac 1 {n^r} \sum_{k \mathop = 0}^{n - 1} \sum_{j \mathop = 1}^\infty \paren {\frac 1 {j^r} - \frac 1 {\paren {j + \paren {\dfrac {x - k} n} }^r} }
      | c = {{Defof|General Harmonic Numbers}}
}}
{{eqn | r = \sum_{j \mathop = 1}^\infty \frac 1 {j^r} - \sum_{j \mathop = 1}^{\infty} \frac 1 {\paren {j + x}^r} - \dfrac 1 {n^r} \sum_{k \mathop = 0}^{n - 1} \sum_{j \mathop = 1}^\infty \frac 1 {j^r} + \dfrac 1 {n^r} \sum_{k \mathop = 0}^{n - 1} \sum_{j \mathop = 1}^\infty \frac 1 {\paren {j + \paren {\dfrac {x - k} n} }^r}
      | c = Sum of Absolutely Convergent Series
}}
{{eqn | r = \sum_{j \mathop = 1}^\infty \frac 1 {j^r} - \sum_{j \mathop = 1}^\infty \frac 1 {\paren {j + x}^r} - \dfrac n {n^r} \sum_{j \mathop = 1}^\infty \frac 1 {j^r} + \sum_{k \mathop = 0}^{n - 1} \sum_{j \mathop = 1}^\infty \frac 1 {\paren {n j - k + x }^r}
      | c = simplifying
}}
{{eqn | r = \map \zeta r - \sum_{j \mathop = 1}^\infty \frac 1 {\paren {j + x}^r} - \dfrac n {n^r} \map \zeta r + \sum_{k \mathop = 0}^{n - 1} \sum_{j \mathop = 1}^\infty \frac 1 {\paren {n j - k + x }^r}
      | c = {{Defof|Riemann Zeta Function}}
}}
{{eqn | r = \map \zeta r - \dfrac n {n^r} \map \zeta r
      | c = {{Lemma|Sum of General Harmonic Numbers in terms of Riemann Zeta Function}}
}}
{{eqn | r = \paren {1 - n^{1 - r} } \map \zeta r
      | c = simplifyiing
}}
{{end-eqn}}
{{qed}}
Theorem: Conservative Force gives rise to Two Forms of Energy

Let $E$ be a energy which has come about as a result of a conservative force.
Then $E$ comes in two forms:
:$(1): \quad$ Kinetic energy
:$(2): \quad$ Potential energy.

Proof:
{{ProofWanted|don't even know what this means}}
Theorem: Category of Locales is Category

Let $\mathbf{Loc}$ denote the category of locales.
Then:
:$\mathbf{Loc}$ is a category

Proof:
By definition, the category of locales is:
:the dual category of the category of frames
From Category of Frames is Category:
:the category of frames is a category
From Dual Category is Category:
:the category of locales is a category
{{qed}}
Theorem: Category of Frames is Category

Let $\mathbf{Frm}$ denote the category of frames.
Then:
:$\mathbf{Frm}$ is a metacategory

Proof:
Let us verify the axioms $(\text C 1)$ up to $(\text C 3)$ for a metacategory.
For any two frame homomorphisms their composition (in the usual set theoretic sense) is again a frame homomorphism by Composite Frame Homomorphism is Frame Homomorphism.
For any frame $L = \struct{S, \preceq}$, we have the identity mapping $\operatorname{id}_S$.
From Identity Mapping is Frame Homomorphism we have $\operatorname{id}_S$ is a frame homomorphism.
By Identity Mapping is Left Identity and Identity Mapping is Right Identity, this is the identity morphism for $L$.
Finally by Composition of Mappings is Associative, the associative property is satisfied.
Hence $\mathbf{Frm}$ is a metacategory.
{{qed}}
Theorem: Equation of Epitrochoid

Let a circle $C_1$ of radius $b$ roll around the outside of another circle $C_2$ of radius $a$.
Consider a point $P$ on the line of a radius of $C_1$ at a distance $d$ from the center of $C_1$.
Let $C_2$ be embedded in a cartesian plane with its center $O$ located at the origin.
Let $P$ be a point on the circumference of $C_1$.
Let $C_1$ be initially positioned so that $P$ is its point of tangency to $C_2$, located at point $A = \tuple {a, 0}$ on the $x$-axis.
Let $H$ be the epitrochoid traced out by the point $P$.
Let $\tuple {x, y}$ be the coordinates of $P$ as it travels over the plane.
The point $P = \tuple {x, y}$ is described by the equations:
{{begin-eqn}}
{{eqn | l = x
      | r = \paren {a + b} \cos \theta - d \map \cos {\paren {\dfrac {a + b} b} \theta}
}}
{{eqn | l = y
      | r = \paren {a + b} \sin \theta - d \map \sin {\paren {\dfrac {a + b} b} \theta}
}}
{{end-eqn}}

Proof:
:600px
Let $C_1$ have rolled so that the line $OC$ through the radii of $C_1$ and $C_2$ is at angle $\theta$ to the $x$-axis.
Let $C_1$ have turned through an angle $\phi$ to reach that point.
By definition of sine and cosine, $P = \tuple {x, y}$ is defined by:
{{begin-eqn}}
{{eqn | l = x
      | r = \paren {a + b} \cos \theta - d \map \cos {\phi + \theta}
}}
{{eqn | l = y
      | r = \paren {a + b} \sin \theta - d \map \sin {\phi + \theta}
}}
{{end-eqn}}
The arc of $C_1$ between $P$ and $B$ is the same as the arc of $C_2$ between $A$ and $B$.
Thus by Arc Length of Sector:
:$a \theta = b \phi$
Thus:
:$\phi + \theta = \paren {\dfrac {a + b} b} \theta$
whence the result.
{{qed}}
Theorem: Recurrence Relation for General Harmonic Numbers

:$\harm r x = \harm r {x - 1} + \dfrac 1 {x^r}$

Proof:
{{begin-eqn}}
{{eqn | l = \harm r x
	  | r = \sum_{k \mathop = 1}^{\infty} \paren {\frac 1 {k^r} - \frac 1 {\paren {k + x}^r} }
      | c = {{Defof|General Harmonic Numbers}}
}}
{{eqn | r = \sum_{k \mathop = 1}^{\infty} \paren {\frac 1 {k^r} - \frac 1 {\paren {k + x}^r} } - \dfrac 1 {x^r} + \dfrac 1 {x^r}
      | c = add $0$
}}
{{eqn | r = \sum_{k \mathop = 1}^{\infty} \paren {\frac 1 {k^r} - \frac 1 {\paren {\paren {k - 1} + x }^r} } + \dfrac 1 {x^r}
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 1}^{\infty} \paren {\frac 1 {k^r} - \frac 1 {\paren {k + \paren {x - 1} }^r} } + \dfrac 1 {x^r}
      | c = 
}}
{{eqn | r = \harm r {x - 1} + \dfrac 1 {x^r}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: General Harmonic Number Additive Formula

:$\ds \harm 1 {n x} = \frac 1 n \sum_{k \mathop = 0}^{n - 1} \paren {\harm 1 {x - \dfrac k n } } + \ln n$

Proof:
{{begin-eqn}}
{{eqn | l = \map \psi {n z}
      | r = \frac 1 n \sum_{k \mathop = 0}^{n - 1} \map \psi {z + \frac k n} + \ln n
      | c = Digamma Additive Formula
}}
{{eqn | ll= \leadsto
      | l = \paren {-\gamma + \harm 1 {n z - 1} }
      | r = \frac 1 n \sum_{k \mathop = 0}^{n - 1} \paren {-\gamma + \harm 1 {z + \dfrac k n - 1} } + \ln n
      | c = Digamma Function in terms of General Harmonic Number: $\map \psi {z + 1} = -\gamma + \harm 1 z$
}}
{{eqn | r = \frac 1 n \paren {-n \gamma} + \frac 1 n \sum_{k \mathop = 0}^{n - 1} \paren {\harm 1 {z + \dfrac k n - 1} } + \ln n
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \harm 1 {n z - 1}
      | r = \frac 1 n \sum_{k \mathop = 0}^{n - 1} \paren {\harm 1 {z + \dfrac k n - 1} } + \ln n
      | c = adding $\gamma$ from both sides
}}
{{eqn | ll= \leadsto
      | l = \harm 1 {n x}
      | r = \frac 1 n \sum_{k \mathop = 0}^{n - 1} \paren {\harm 1 {x + \dfrac 1 n + \dfrac k n - 1} } + \ln n
      | c = let $\paren {n z - 1} \to n x$
}}
{{eqn | r = \frac 1 n \paren {\harm 1 {x - \dfrac {\paren {n - 1} } n} + \harm 1 {x - \dfrac {\paren {n - 2} } n } + \cdots + \harm 1 {x - \dfrac {\paren {n - n} } n} } + \ln n
      | c = 
}}
{{eqn | r = \frac 1 n \paren {\harm 1 {x - \dfrac {\paren {n - n} } n} + \harm 1 {x - \dfrac {\paren {n - \paren {n - 1} } } n } + \cdots + \harm 1 {x - \dfrac {\paren {n - 1} } n} } + \ln n
      | c = reversing the order of the sum
}}
{{eqn | r = \frac 1 n \sum_{k \mathop = 0}^{n - 1} \paren {\harm 1 {x - \dfrac k n} } + \ln n
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Boolean Algebra as Boolean Lattice

Let $\struct {S, \vee, \wedge, \neg}$ be a Boolean algebra.
Then, there is a unique ordering $\preceq$ on $S$ such that:
:$\struct {S, \vee, \wedge, \preceq}$ is a Boolean lattice
In particular, it can be defined by:
:$a \preceq b \iff a \vee b = b$
for all $a, b \in S$.

Proof:
First, we will show that the given ordering indeed forms a Boolean lattice.
{{Recall|Boolean Lattice|index = 2}}
{{:Definition:Boolean Lattice/Definition 2}}
{{Recall|Ordered Structure}}
{{:Definition:Ordered Structure}}
Hence it suffices to show that:
:$(1): \quad \preceq$ is in fact an ordering
:$(2): \quad \preceq$ is compatible with $\vee$ and $\wedge$
:$(3): \quad$ For all $a, b \in S: a \wedge b \preceq a \vee b$
Theorem: Geometric Congruence is Equivalence Relation

Let $S$ be the set of geometric figures.
For $F_1, F_2 \in S$, let $F_1 \cong F_2$ denote that $F_1$ is congruent to $F_2$.
Then $\cong$ is an equivalence relation on $S$.

Proof:
{{tidy}}
Checking in turn each of the criteria for equivalence:
Theorem: Nth Derivative of General Harmonic Number Order One

:$\dfrac {\d^n} {\d x^n} \harm 1 x = \paren {-1}^{n + 1} n! \paren {\map \zeta {n + 1} - \harm {n + 1} x}$

Proof:
{{begin-eqn}}
{{eqn | l = \dfrac {\d^n} {\d x^n} \harm 1 x
      | r = \dfrac {\d^n} {\d x^n} \paren {\sum_{k \mathop = 1}^\infty \paren {\frac 1 {k^1} - \frac 1 {\paren {k + x}^1} } }
	    | c = {{Defof|General Harmonic Numbers}}
}}
{{eqn | r = \dfrac {\d^n} {\d x^n} \paren {\sum_{k \mathop = 1}^\infty \frac 1 {k^1} } - \dfrac {\d^n} {\d x^n} \paren {\sum_{k \mathop = 1}^\infty \frac 1 {\paren {k + x}^1} }
      | c = Linear Combination of Convergent Series
}}
{{eqn | r = \paren {-1}^{n + 1} n! \paren {\sum_{k \mathop = 1}^\infty \frac 1 {\paren {k + x}^{n + 1} } }
      | c = {{Corollary|Nth Derivative of Reciprocal of Mth Power}}
}}
{{eqn | r = \paren {-1}^{n + 1} n! \paren {\paren {\sum_{k \mathop = 1}^\infty \frac 1 {k^{n + 1} } - \sum_{k \mathop = 1}^\infty \frac 1 {k^{n + 1} } } + \sum_{k \mathop = 1}^\infty \frac 1 {\paren {k + x}^{n + 1} } }
      | c = add $0$
}}
{{eqn | r = \paren {-1}^{n + 1} n! \paren {\sum_{k \mathop = 1}^\infty \frac 1 {k^{n + 1} } - \sum_{k \mathop = 1}^\infty \paren {\frac 1 {k^{n + 1} } - \frac 1 {\paren {k + x}^{n + 1} } } }
      | c = 
}}
{{eqn | r = \paren {-1}^{n + 1} n! \paren {\map \zeta {n + 1} - \harm {n + 1} x}
      | c = {{Defof|Riemann Zeta Function}}
}}
{{end-eqn}}
{{qed}}
Category:Derivatives
Category:General Harmonic Numbers
o7od5gz0icgt3o97o8ohts2mavny5sh
Theorem: General Harmonic Number Reflection Formula

:$\harm r {x - 1} + \paren {-1}^r \harm r {-x} = \paren {1 + \paren {-1}^r} \map \zeta r + \dfrac {\paren {-1}^r} {\paren {r - 1}!} \map {\dfrac {\d^{r - 1} } {\d x^{r - 1} } } {\pi \map \cot {\pi x} }$

Proof:
=== Lemma 1 ===
{{:General Harmonic Number Reflection Formula/Lemma 1}}{{qed|lemma}}
Theorem: Composite Frame Homomorphism is Frame Homomorphism

Let $L_1 = \struct{S_1, \preceq_1}$, $L_2 = \struct{S_2, \preceq_2}$ and $L_3 = \struct{S_3, \preceq_3}$ be frames.
Let $\phi_1: L_1 \to L_2$ and $\phi_2: L_2 \to L_3$ be frame homomorphisms.
Let $\phi_2 \circ \phi_1 : S_1 \to S_3$ be the composite mapping of $\phi_1$ and $\phi_2$  
Then:
:$\phi_2 \circ \phi_1$ is a frame homomorphism of $L_1$ to $L_3$

Proof:
=== $\phi_2 \circ \phi_1$ is Finite Meet Preserving ===
Let $F \subseteq S_1$ be a finite subset.
We have:
{{begin-eqn}}
{{eqn | l = \inf \paren {\phi_2 \circ \phi_1} \sqbrk F
      | r = \inf \phi_2 \sqbrk {\phi_1 \sqbrk F}
      | c = Image of Subset under Composite Relation with Common Codomain and Domain
}}
{{eqn | r = \map {\phi_2} {\inf \phi_1 \sqbrk F }
      | c = {{Defof|Finite Meet Preserving Mapping}}
}}
{{eqn | r = \map {\phi_2} {\map {\phi_1} {\inf F} }
      | c = {{Defof|Finite Meet Preserving Mapping}}
}}
{{eqn | r = \map {\paren{\phi_2 \circ \phi_1} } {\inf F}
      | c = {{Defof|Composite Mapping}}
}}
{{end-eqn}}
Since $F$ was arbitrary, it follows that $\phi_2 \circ \phi_1$ is finite meet preserving by definition.
{{qed|lemma}}
Theorem: Identity Mapping is Frame Homomorphism

Let $L = \struct{S, \preceq}$ be a frame.
Let $\operatorname{id}_S$ denote the identity mapping on $S$.
Then:
:$\operatorname{id}_S$ is a frame homomorphism of $L$ to $L$

Proof:
=== $\operatorname{id}_S$ is Finite Meet Preserving ===
Let $F \subseteq S_1$ be a finite subset.
We have:
{{begin-eqn}}
{{eqn | l = \inf \operatorname{id}_S \sqbrk F
      | r = \inf F
      | c = {{Defof|Identity Mapping}}
}}
{{eqn | r = \map {\operatorname{id}_S} {\inf F}
      | c = {{Defof|Identity Mapping}}
}}
{{end-eqn}}
Since $F$ was arbitrary, it follows that $\operatorname{id}_S$ is finite meet preserving by definition.
{{qed|lemma}}
Theorem: Escape Speed in terms of Universal Gravitational Constant

Let $P$ be a planet.
Let $P$ have:
:a mass of $M$
:a radius of $R$.
Then the escape speed of $P$ is given by:
:$V = \sqrt {\dfrac {2 M G} R}$
where $G$ is the universal gravitational constant.

Proof:
Let $b$ be a particle with mass $m$.  
Let $K_i$ be the kinetic energy of $b$ at the surface of $P$.  
Let $U_i$ be the potential energy of $b$ at the surface of $P$. 
Let $K_f$ be the limit of the kinetic energy of $b$ as it leaves $P$. 
Let $U_f$ be the limit of the potential energy of $b$ as it leaves $P$. 
Let $v_f$ be the limit of the speed of $b$ as it leaves $P$. 
Let $r_f$ be the limit of the distance of $b$ from the center of $P$ as $b$ leaves $P$. 
Let $v_e$ be the speed of $b$ at the surface of $P$.  
The speed of $b$ becomes arbitarily small as it leaves $P$.
Thus:
:$v_f = 0$
The distance of $b$ to the center of $P$ becomes arbitarily large as it leaves $P$.
Thus:
:$r_f = \infty$
By Kinetic Energy of Motion: 
{{begin-eqn}}
{{eqn | l = K_i
      | r = \frac 1 2 m {v_e}^2
      | c = 
}}
{{eqn | l = K_f
      | r = \frac 1 2 m {v_f}^2
      | c = 
}}
{{eqn | r = \frac 1 2 m \paren 0^2
      | c = 
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
By Gravitational Potential Energy of Position for Bodies Far From Center:
{{begin-eqn}}
{{eqn | l = U_i
      | r = -\frac {G M m} R
      | c = 
}}
{{eqn | l = U_f
      | r = 0
      | c = 
}}
{{end-eqn}}
Now:
{{begin-eqn}}
{{eqn | l = K_i + U_i
      | r = K_f + U_f
      | c = Principle of Conservation of Energy
}}
{{eqn | l = \frac 1 2 m {v_e}^2 - \frac {G M m} R
      | r = 0
      | c = substitution
}}
{{eqn | l = v_e
      | r = \sqrt {\frac {2 G M} R}
      | c = after algebra
}}
{{end-eqn}}
{{qed}}
Theorem: Characterization of Compact Element in Complete Lattice

Let $L = \struct{S, \preceq}$ be a complete lattice.
Let $a \in S$.
{{TFAE}}:
:$(1)\quad a$ is a compact element
:$(2)\quad \forall I \subseteq S : I$ is an ideal $: a \preceq \sup I \implies a \in I$
:$(3)\quad \forall A \subseteq S : a \preceq \sup A \implies \exists F \subseteq A : F$ is finite $: a \preceq \sup F$

Proof:
Recall, $a$ is a compact element {{iff}}:
:for every directed subset $D$ of $S$ such that $a \preceq \sup D$
::$\exists d \in D: a \preceq d$
Theorem: Characterization of Compact Element in Frame or Locale

Let $L = \struct{S, \preceq}$ be a frame or locale.
Let $a \in S$.
{{TFAE}}:
:$(1)\quad a$ is a compact element
:$(2)\quad \forall I \subseteq S : I$ is an ideal $: a \preceq \sup I \implies a \in I$
:$(3)\quad \forall A \subseteq S : a \preceq \sup A \implies \exists F \subseteq A : F$ is finite $: a \preceq \sup F$ 
:$(4)\quad \forall A \subseteq S : a = \sup A \implies \exists F \subseteq A : F$ is finite $: a = \sup F$

Proof:
Recall, a frame or locale is a complete lattice satisfying the infinite join distributive law:
{{:Axiom:Infinite Join Distributive Law}}
From Characterization of Compact Element in Complete Lattice:
:Statements $(1)$, $(2)$ and $(3)$ are equivalent.
Theorem: Reciprocal of Difference of Squares as Sum of Reciprocals

:$\dfrac 1 {x^2 - y^2} = \dfrac 1 {2 x \paren {x + y} } + \dfrac 1 {2 x \paren {x - y} }$

Proof:
{{begin-eqn}}
{{eqn | l = \dfrac 1 {x + y} + \dfrac 1 {x - y}
      | r = \dfrac {\paren {x - y} + \paren {x + y} } {\paren {x - y} \paren {x + y} }
      | c = putting everything over a common denominator
}}
{{eqn | r = \dfrac {2 x} {x^2 - y^2}
      | c = simplifying, and Difference of Two Squares
}}
{{eqn | ll= \leadsto
      | l = \dfrac 1 {2 x \paren {x + y} } + \dfrac 1 {2 x \paren {x - y} }
      | r = \dfrac 1 {x^2 - y^2}
      | c = dividing both sides by $2 x$
}}
{{end-eqn}}
{{qed}}
Theorem: Reciprocal of Difference of Squares as Difference of Reciprocals

:$\dfrac 1 {x^2 - y^2} = \dfrac 1 {2 y \paren {x - y} } - \dfrac 1 {2 y \paren {x + y} }$

Proof:
{{begin-eqn}}
{{eqn | l = \dfrac 1 {x - y} - \dfrac 1 {x + y}
      | r = \dfrac {\paren {x + y} - \paren {x - y} } {\paren {x + y} \paren {x - y} }
      | c = putting everything over a common denominator
}}
{{eqn | r = \dfrac {2 y} {x^2 - y^2}
      | c = simplifying, and Difference of Two Squares
}}
{{eqn | ll= \leadsto
      | l = \dfrac 1 {2 y \paren {x - y} } - \dfrac 1 {2 y \paren {x + y} }
      | r = \dfrac 1 {x^2 - y^2}
      | c = dividing both sides by $2 y$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Root of x squared plus a squared over x/Logarithm Form

:$\ds \int \frac {\sqrt {x^2 + a^2} } x \rd x = \sqrt {x^2 + a^2} - a \map \ln {\frac {a + \sqrt {x^2 + a^2} } a} + C$

Proof:
Let:
{{begin-eqn}}
{{eqn | l = z
      | r = x^2
}}
{{eqn | ll= \leadsto
      | l = \frac {\d z} {\d x}
      | r = 2 x
      | c = Power Rule for Derivatives
}}
{{eqn | ll= \leadsto
      | l = \int \frac {\sqrt {x^2 + a^2} } x \rd x
      | r = \int \frac {\sqrt {z + a^2} \rd z} {2 \sqrt z \sqrt z}
      | c = Integration by Substitution
}}
{{eqn | r = \frac 1 2 \int \frac {\sqrt {z + a^2} \rd z} z
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \frac 1 2 \paren {2 \sqrt {z + a^2} + a^2 \int \frac {\d z} {z \sqrt {z + a^2} } } + C
      | c = Primitive of $\dfrac {\sqrt {a x + b} } x$
}}
{{eqn | r = \sqrt {x^2 + a^2} + \frac {a^2} 2 \int \frac {2 x \rd x} {x^2 \sqrt {x^2 + a^2} } + C
      | c = substituting for $z$
}}
{{eqn | r = \sqrt {x^2 + a^2} + a^2 \int \frac {\d x} {x \sqrt {x^2 + a^2} } + C
      | c = simplifying
}}
{{eqn | r = \sqrt {x^2 + a^2} + a^2 \paren {-\frac 1 a \map \ln {\frac {a + \sqrt {x^2 + a^2} } x} } + C
      | c = Primitive of $\dfrac 1 {x \sqrt {x^2 + a^2} }$
}}
{{eqn | r = \sqrt {x^2 + a^2} - a \map \ln {\frac {a + \sqrt {x^2 + a^2} } a} + C
      | c = simplification
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Root of x squared plus a squared over x squared/Logarithm Form

:$\ds \int \frac {\sqrt {x^2 + a^2} } {x^2} \rd x = \frac {-\sqrt {x^2 + a^2} } x + \map \ln {x + \sqrt {x^2 + a^2} } + C$

Proof:
Let:
{{begin-eqn}}
{{eqn | l = z
      | r = x^2
}}
{{eqn | ll= \leadsto
      | l = \frac {\d z} {\d x}
      | r = 2 x
      | c = Power Rule for Derivatives
}}
{{eqn | ll= \leadsto
      | l = \int \frac {\sqrt {x^2 + a^2} } {x^2} \rd x
      | r = \int \frac {\sqrt {z + a^2} \rd z} {2 z \sqrt z}
      | c = Integration by Substitution
}}
{{eqn | r = \frac 1 2 \int \frac {\sqrt {z + a^2} \rd z} {z^{3/2} }
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \frac 1 2 \paren {\frac {-\sqrt {z + a^2} } {\frac 1 2 \sqrt z} + \frac 1 2 \int \frac {\d z} {\sqrt z \sqrt {z + a^2} } } + C
      | c = Primitive of $\dfrac {\sqrt {a x + b} } {x^m}$
}}
{{eqn | r = \frac {-\sqrt {x^2 + a^2} } x + \frac 1 2 \int \frac {2 x \rd x} {x \sqrt {x^2 + a^2} } + C
      | c = substituting for $z$
}}
{{eqn | r = \frac {-\sqrt {x^2 + a^2} } x + \int \frac {\d x} {\sqrt {x^2 + a^2} } + C
      | c = simplifying
}}
{{eqn | r = \frac {-\sqrt {x^2 + a^2} } x + \map \ln {x + \sqrt {x^2 + a^2} } + C
      | c = Primitive of $\dfrac 1 {\sqrt {x^2 + a^2} }$
}}
{{end-eqn}}
{{qed}}
Theorem: Row Rank of Matrix equals Rank of Matrix

Let $\mathbf A$ be a matrix.
The row rank of $\mathbf A$ is equal to the rank of $\mathbf A$.

Proof:
The rank of $\mathbf A$ is defined as the dimension of the column space of $\mathbf A$.
That is, the rank of $\mathbf A$ is the column rank of $\mathbf A$.
The result follows from Column Rank of Matrix equals Row Rank.
{{qed}}