avewright/proofwiki-math huggingface dataset:
Theorem: Integration by Parts/Primitive

:$\ds \int \map f t \map G t \rd t = \map F t \map G t - \int \map F t \map g t \rd t$
on $\closedint a b$.

Proof:
Let $\map u x$ and $\map v x$ be integrable functions defined on $\closedint a b$.
Then:
{{begin-eqn}}
{{eqn | l = \map {\dfrac \d {\d x} } {u v}
      | r = u \dfrac {\d v} {\d x} + v \dfrac {\d u} {\d x}
      | c = Product Rule for Derivatives
}}
{{eqn | ll= \leadsto
      | l = v \dfrac {\d u} {\d x}
      | r = \map {\dfrac \d {\d x} } {u v} - u \dfrac {\d v} {\d x}
      | c = rearranging
}}
{{eqn | ll= \leadsto
      | l = \int v \dfrac {\d u} {\d x} \rd x
      | r = \int \paren {\map {\dfrac \d {\d x} } {u v} - u \dfrac {\d v} {\d x} } \rd x
      | c = integrating both sides {{WRT|Integration}} $x$
}}
{{eqn | r = \int \map {\dfrac \d {\d x} } {u v} \rd x - \int u \dfrac {\d v} {\d x} \rd x
      | c = Linear Combination of Primitives
}}
{{eqn | r = u v - \int u \dfrac {\d v} {\d x} \rd x
      | c = Fundamental Theorem of Calculus
}}
{{end-eqn}}
{{qed}}
Theorem: Integration by Substitution/Definite Integral

If $\map \phi a \le \map \phi b$, then the definite integral of $f$ from $a$ to $b$ can be evaluated by:
:$\ds \int_{\map \phi a}^{\map \phi b} \map f t \rd t = \int_a^b \map f {\map \phi u} \dfrac \d {\d u} \map \phi u \rd u$
where $t = \map \phi u$.
If $\map \phi a > \map \phi b$, then the definite integral of $f$ from $a$ to $b$ can be evaluated by:
:$\ds - \int_{\map \phi b}^{\map \phi a} \map f t \rd t = \int_a^b \map f {\map \phi u} \dfrac \d {\d u} \map \phi u \rd u$

Proof:
Let $F$ be an antiderivative of $f$.
We have:
{{begin-eqn}}
{{eqn | l = \map {\frac \d {\d u} } {\map F t}
      | r = \map {\frac \d {\d u} } {\map F {\map \phi u} }
      | c = Definition of $\map \phi u$
}}
{{eqn | r = \dfrac \d {\d t} \map F {\map \phi u} \dfrac \d {\d u} \map \phi u
      | c = Chain Rule for Derivatives
}}
{{eqn | r = \map f {\map \phi u} \dfrac \d {\d u} \map \phi u
      | c = as $\map F t = \ds \int \map f t \rd t$
}}
{{end-eqn}}
Hence $\map F {\map \phi u}$ is an antiderivative of $\map f {\map \phi u} \dfrac \d {\d u} \map \phi u$.
Thus:
{{begin-eqn}}
{{eqn | l = \int_a^b \map f {\map \phi u} \map {\phi'} u \rd u
      | r = \bigintlimits {\map F {\map \phi u} } a b
      | c = Fundamental Theorem of Calculus: Second Part
}}
{{eqn | n = 1
      | r = \map F {\map \phi b} - \map F {\map \phi a}
      | c = 
}}
{{end-eqn}}
If $\map \phi a \le \map \phi b$, we also have:
{{begin-eqn}}
{{eqn | l = \int_{\map \phi a}^{\map \phi b} \map f t \rd t
      | r = \bigintlimits {\map F t} {\map \phi a} {\map \phi b}
      | c = 
}}
{{eqn | r = \map F {\map \phi b} - \map F {\map \phi a}
      | c = 
}}
{{eqn | r = \int_a^b \map f {\map \phi u} \map {\phi'} u \rd u
      | c = from $(1)$
}}
{{end-eqn}}
which was to be proved. 
If instead $\map \phi a > \map \phi b$, we have:
{{begin-eqn}}
{{eqn | l = - \int_{\map \phi b}^{\map \phi a} \map f t \rd t
      | r = - \bigintlimits {\map F t} {\map \phi b} {\map \phi a}
      | c = 
}}
{{eqn | r = \map F {\map \phi b} - \map F {\map \phi a}
      | c = 
}}
{{eqn | r = \int_a^b \map f {\map \phi u} \map {\phi'} u \rd u
      | c = from $(1)$
}}
{{end-eqn}}
which was to be proved.
{{qed}}
Theorem: Product Formula for Norms on Non-zero Rationals/Lemma

Let $z \in \Z_{\ne 0}$.
Then the following infinite product converges:
:$\size z \times \ds \prod_{p \mathop \in \Bbb P}^{} \norm z_p = 1$

Proof:
=== Case 1 : $z \in \Z_{>0}$ ===
Let $z \in \Z_{>0}$.
From Fundamental Theorem of Arithmetic, we can factor $z$ as a product of one or more primes:
:$z = p_1^{b_1} p_2^{b_2} \dots p_k^{b_k}$
Then for every prime number $q$:
:$\norm z_q = \begin{cases}
p_i^{-b_i} & : \exists i \in \closedint 1 k :q = p_i \\
1 & : \forall i \in \closedint 1 k : q \ne p_i \\
\end {cases}$
By definition of absolute value on $\Q$:
:$\size z = p_1^{b_1} p_2^{b_2} \dots p_k^{b_k} $
For $n \ge \max \set{p_1, p_2 \dots p_k}$:
{{begin-eqn}}
{{eqn | l = \size z \times \prod_{p \mathop \in \Bbb P \mathop : p \mathop \le n } \norm z_p
      | r = \paren {p_1^{b_1} p_2^{b_2} \dots p_k^{b_k} } \times \paren {p_1^{-b_1} p_2^{-b_2} \dots p_k^{-b_k} } 
}}
{{eqn | r = 1
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = \size z \times \prod_{p \mathop\in \Bbb P} \norm z_p
      | r = \lim_{n \mathop \to \infty} \paren{\size z \times \prod_{p \mathop \in \Bbb P \mathop : p \mathop \le n} \norm z_p}
      | c = {{Defof|Infinite Product}}
}}
{{eqn | r = 1
      | c = Eventually Constant Sequence Converges to Constant
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: P-adic Open Ball is Instance of Open Ball of a Norm

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $a \in \Q_p$.
Let $\epsilon \in \R_{>0}$ be a strictly positive real number.
Let $B \subseteq \Q_p$.
Then: 
:$B$ is an open ball in $p$-adic numbers with radius $\epsilon$ and centre $a$
{{iff}}:
:$B$ is an open ball of the normed division ring $\struct {\Q_p, \norm {\,\cdot\,}_p}$ with radius $\epsilon$ and centre $a$ .
That is, the definition of an open ball in $p$-adic numbers is a specific instance of the general definition of an open ball in a normed division ring.

Proof:
From P-adic Numbers form Non-Archimedean Valued Field:
:the $p$-adic numbers $\struct {\Q_p, \norm {\,\cdot\,}_p}$ form a non-Archimedean valued field.
The definition of an open ball in $p$-adic numbers is identical to the definition of an open ball of a normed division ring with respect to the norm $\norm {\,\cdot\,}_p$.
{{qed}}
Category:Open Balls 
Category:P-adic Number Theory
n72sday0r0i661ntww1la2eldja7481
Theorem: P-adic Closed Ball is Instance of Closed Ball of a Norm

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $a \in \Q_p$.
Let $\epsilon \in \R_{>0}$ be a strictly positive real number.
Let $B \subseteq \Q_p$.
Then: 
:$B$ is a closed ball in $p$-adic numbers with radius $\epsilon$ and centre $a$
{{iff}}:
:$B$ is a closed ball of the normed division ring $\struct {\Q_p, \norm {\,\cdot\,}_p}$ with radius $\epsilon$ and centre $a$ 
That is, the definition of a closed ball in $p$-adic numbers is a specific instance of the general definition of a closed ball in a normed division ring.

Proof:
From P-adic Numbers form Non-Archimedean Valued Field:
:the $p$-adic numbers $\struct {\Q_p, \norm {\,\cdot\,}_p}$ form a non-Archimedean valued field.
The definition of a closed ball in $p$-adic numbers is identical to the definition of a closed ball of a normed division ring with respect to the norm $\norm {\,\cdot\,}_p$.
{{qed}}
Category:P-adic Number Theory
eg9w16nkehq3s68xarfpq0s71huzxjq
Theorem: P-adic Sphere is Instance of Sphere of a Norm

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $a \in \Q_p$.
Let $\epsilon \in \R_{>0}$ be a strictly positive real number.
Let $S \subseteq \Q_p$.
Then: 
:$S$ is a sphere in $p$-adic numbers with radius $\epsilon$ and centre $a$
{{iff}}:
:$S$ is a sphere of the normed division ring $\struct {\Q_p, \norm {\,\cdot\,}_p}$ with radius $\epsilon$ and centre $a$ 
That is, the definition of a closed ball in $p$-adic numbers is a specific instance of the general definition of a sphere in a normed division ring.

Proof:
From P-adic Numbers form Non-Archimedean Valued Field:
:the $p$-adic numbers $\struct {\Q_p, \norm {\,\cdot\,}_p}$ form a non-Archimedean valued field.
The definition of a sphere in $p$-adic numbers is identical to the definition of a sphere in a normed division ring with respect to the norm $\norm {\,\cdot\,}_p$.
{{qed}}
Category:P-adic Number Theory
qd84tqy5qzif9gowqvb02s4697fp6xq
Theorem: Sphere is Set Difference of Closed Ball with Open Ball/P-adic Numbers

Let $p$ be a prime number.
Let $\struct{\Q_p,\norm{\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $a \in \Q_p$.
Let $\epsilon \in \R_{>0}$ be a strictly positive real number.
Let $\map {{B_\epsilon}^-} a$ denote the $\epsilon$-closed ball of $a$ in $\Q_p$.
Let $\map {B_\epsilon} a$ denote the $\epsilon$-open ball of $a$ in $\Q_p$.
Let $\map {S_\epsilon} a$ denote the $\epsilon$-sphere of $a$ in $\Q_p$.
Then:
:$\map {S_\epsilon} a = \map { {B_\epsilon}^-} a \setminus \map {B_\epsilon} a$

Proof:
The result follows directly from:
:P-adic Closed Ball is Instance of Closed Ball of a Norm
:P-adic Open Ball is Instance of Open Ball of a Norm
:P-adic Sphere is Instance of Sphere of a Norm
:Sphere is Set Difference of Closed and Open Ball in Normed Division Ring
{{qed}}
Category:P-adic Number Theory
arvlbze0xra6eabckm871813pj10bre
Theorem: Set is Closed in Metric Space iff Closed in Induced Topological Space

Let $M = \struct {A, d}$ be a metric space.
Let $\tau$ be the topology induced by the metric $d$.
Let $F$ be a subset of $M$.
Then:
:$F$ is closed in $M$ {{iff}} $F$ is closed in $\struct {A, \tau}$

Proof:
By definition of a closed set in $M$:
:$F$ is closed set in $M$ {{iff}} $A \setminus F$ is open in $M$
By definition of the topology $\tau$ induced by the metric $d$:
:$A \setminus F$ is open in $M$ {{iff}} $A \setminus F$ is open in $\struct {A, \tau}$
By definition of a closed set in $\struct{A, \tau}$:
:$A \setminus F$ is open in $\struct {A, \tau}$ {{iff}} $F$ is closed set in $\struct {A, \tau}$
The result follows.
{{qed}}
Category:Closed Sets
Category:Metric Spaces
l4ycvi1ahs62ph5bgwvds2evtt68snc
Theorem: Primitive of Hyperbolic Cosecant Function/Inverse Hyperbolic Cotangent of Hyperbolic Cosine Form

:$\ds \int \csch x \rd x = -\map {\coth^{-1} } {\cosh x} + C$

Proof:
Let:
{{begin-eqn}}
{{eqn | l = u
      | r = \cosh x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\d u} {\d x}
      | r = \sinh x
      | c = Derivative of Hyperbolic Cosine
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \csch x \rd x
      | r = \int \dfrac {\d x} {\sinh x}
      | c = {{Defof|Hyperbolic Cosecant|index = 2}}
}}
{{eqn | r = \int \dfrac 1 {\sinh x} \dfrac {\d u} {\sinh x}
      | c = Integration by Substitution
}}
{{eqn | r = \int \dfrac {\d u} {\sinh^2 x}
      | c = simplifying
}}
{{eqn | r = \int \dfrac {\d u} {\cosh^2 x - 1}
      | c = Difference of Squares of Hyperbolic Cosine and Sine
}}
{{eqn | r = \int \dfrac {\d u} {u^2 - 1}
      | c = Definition of $u$
}}
{{eqn | r = -\coth^{-1} u + C
      | c = Primitive of $\dfrac 1 {x^2 - a^2}$: $\coth^{-1}$ form
}}
{{eqn | r = -\map {\coth^{-1} } {\cosh x} + C
      | c = Definition of $u$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Hyperbolic Cosecant Function/Inverse Hyperbolic Cotangent of Hyperbolic Cosine Form

:$\ds \int \csch x \rd x = -\map {\coth^{-1} } {\cosh x} + C$

Proof:
Let:
{{begin-eqn}}
{{eqn | l = u
      | r = \cosh x
}}
{{eqn | ll= \leadsto
      | l = u'
      | r = \sinh x
      | c = Derivative of Hyperbolic Cosine
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \csch x \rd x
      | r = \int \frac 1 {\sinh x} \rd x
      | c = {{Defof|Hyperbolic Cosecant}}
}}
{{eqn | r = \int \frac {\sinh x} {\sinh^2 x} \rd x
      | c = multiplying top and bottom by $\sinh x$
}}
{{eqn | r = \int \frac {\sinh x} {\cosh^2 x - 1} \rd x
      | c = Difference of Squares of Hyperbolic Cosine and Sine
}}
{{eqn | r = \int \frac {\rd u} {u^2 - 1}
      | c = Integration by Substitution
}}
{{eqn | r = -\coth^{-1} u + C
      | c = Primitive of Reciprocal of $\dfrac 1 {x^2 - a^2}$: $\coth^{-1}$ form
}}
{{eqn | r = -\map {\coth^{-1} } {\cosh x} + C
      | c = Definition of $u$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of Root of a squared minus x squared/Arccosine Form

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

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac 1 {\sqrt {a^2 - x^2} } \rd x
      | r = \int \frac {\rd x} {\sqrt {a^2 \paren {1 - \frac {x^2} {a^2} } } } 
      | c = factor $a^2$ out of the radicand
}}
{{eqn | r = \int \frac {\rd x} {\sqrt{a^2} \sqrt {1 - \paren {\frac x a}^2} }
      | c = 
}}
{{eqn | r = \frac 1 a \int \frac {\rd x} {\sqrt {1 - \paren {\frac x a}^2} }
}}
{{end-eqn}}
Substitute:
:$\cos \theta = \dfrac x a \iff x = a \cos \theta$
for $\theta \in \openint 0 \pi$.
From Real Cosine Function is Bounded and Shape of Cosine Function, this substitution is valid for all $x / a \in \openint {-1} 1$.
By hypothesis:
{{begin-eqn}}
{{eqn | l = a^2
      | o = > 
      | m = x^2
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = 1
      | o = >
      | m = \frac {x^2} {a^2}
      | c = dividing both terms by $a^2$
}}
{{eqn | ll= \leadstoandfrom
      | l = 1
      | o = >
      | m = \paren {\frac x a}^2
      | c = Powers of Group Elements
}}
{{eqn | ll= \leadstoandfrom
      | l = 1
      | o = >
      | m = \size {\frac x a}
      | c = taking the square root of both terms
}}
{{eqn | ll= \leadstoandfrom
      | l = -1
      | o = <
      | m = \frac x a
      | mo= <
      | r = 1
      | c = Negative of Absolute Value
}}
{{end-eqn}}
so this substitution will not change the domain of the integrand.
Then:
{{begin-eqn}}
{{eqn | l = x 
      | r = a \cos \theta
      | c = from above
}}
{{eqn | ll= \leadsto
      | l = 1
      | r = -a \sin \theta \frac {\rd \theta} {\rd x}
      | c = differentiating {{WRT|Differentiation}} $x$, Derivative of Cosine Function, Chain Rule for Derivatives
}}
{{eqn | l = \frac 1 a \int \frac 1 {\sqrt {1 - \paren {\frac x a}^2 } } \rd x
      | r = \frac 1 a \int \frac {-a \sin \theta} {\sqrt {1 - \cos^2 \theta} } \frac {\rd \theta} {\rd x} \rd x
      | c = from above
}}
{{eqn | r = -\frac a a \int \frac {\sin \theta} {\sqrt {1 - \cos^2 \theta} } \rd \theta
      | c = Integration by Substitution
}}
{{eqn | r = -\int \frac {\sin \theta} {\sqrt {\sin^2 \theta} } \rd \theta
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = -\int \frac {\sin \theta} {\size {\sin \theta} } \rd \theta
      | c = 
}}
{{end-eqn}}
We have defined $\theta$ to be in the open interval $\openint 0 \pi$.
From Sine and Cosine are Periodic on Reals, $\sin \theta > 0$ for the entire interval. Therefore the absolute value is unnecessary, and the integral simplifies to:
{{begin-eqn}}
{{eqn | l = -\int \rd \theta
      | r = -\theta + C
}}
{{end-eqn}}
As $\theta$ was stipulated to be in the open interval $\openint 0 \pi$:
:$\cos \theta = \dfrac x a \iff \theta = \arccos \dfrac x a$
The answer in terms of $x$, then, is:
:$\ds \int \frac 1 {\sqrt {a^2 - x^2} } \rd x = -\arccos \frac x a + C$
{{qed}}
Theorem: Negative of Logarithm of x plus Root x squared minus a squared

Let $x \in \R: \size x > 1$.
Let $x > 1$.
Then:
:$-\map \ln {x + \sqrt {x^2 - a^2} } = \map \ln {x - \sqrt {x^2 - a^2} } - \map \ln {a^2}$

Proof:
First we note that if $x > 1$ then $x + \sqrt {x^2 - a^2} > 0$.
Hence $\map \ln {x + \sqrt {x^2 - a^2} }$ is defined.
Then we have:
{{begin-eqn}}
{{eqn | l = -\map \ln {x + \sqrt {x^2 - a^2} }
      | r = \map \ln {\dfrac 1 {x + \sqrt {x^2 - a^2} } }
      | c = Logarithm of Reciprocal
}}
{{eqn | r = \map \ln {\dfrac {x - \sqrt {x^2 - a^2} } {\paren {x + \sqrt {x^2 - a^2} } \paren {x - \sqrt {x^2 - a^2} } } }
      | c = multiplying top and bottom by $x - \sqrt {x^2 - a^2}$
}}
{{eqn | r = \map \ln {\dfrac {x - \sqrt {x^2 - a^2} } {x^2 - \paren {x^2 - a^2} } }
      | c = Difference of Two Squares
}}
{{eqn | r = \map \ln {\dfrac {x - \sqrt {x^2 - a^2} } {a^2} }
      | c = simplifying
}}
{{eqn | r = \map \ln {x - \sqrt {x^2 - a^2} } - \map \ln {a^2}
      | c = Difference of Logarithms
}}
{{end-eqn}}
{{qed}}
Theorem: Supremum Norm on Vector Space of Real Matrices is Norm

Supremum Norm forms a norm on the vector space of real matrices.

Proof:
Let $M \in \R^{m \times n}: m, n \in \N_{>0}$ be a real matrix.
Denote the $\paren {i, j}$-th entry of $M$ by $a_{i j}$.
Note that the set of matrix elements of $M$ is a finite set of real numbers.
We have that:
:Real Numbers form Totally Ordered Field
:Finite Non-Empty Subset of Ordered Set has Maximal and Minimal Elements
Therefore, $M$ has the greatest element.
Theorem: Arccotangent Logarithmic Formulation

For any real number $x$:
:$\arccot x = -\dfrac i 2 \map \ln {\dfrac {i x - 1} {i x + 1} }$
where $\arccot x$ is the arccotangent and $i^2 = -1$.

Proof:
Assume $y \in \R$, $ -\dfrac \pi 2 \le y \le \dfrac \pi 2 $.
{{begin-eqn}}
{{eqn | l = y
      | r = \arccot x
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = \cot y
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = i \dfrac {e^{i y} + e^{-i y} } {e^{i y} - e^{-i y} }
      | c = Euler's Cotangent Identity
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = i \dfrac {e^{i y} \paren {e^{i y} + e^{-i y} } } {e^{i y} \paren {e^{i y} - e^{-i y} } }
      | c = multiplying top and bottom by $e^{i y}$
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = i \frac {e^{2 i y} + 1} {e^{2 i y} - 1 }
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = i x
      | r = \frac {1 + e^{2 i y} } {1 - e^{2 i y} }
      | c = $ i^2 = -1 $
}}
{{eqn | ll= \leadstoandfrom
      | l = i x \paren {1 - e^{2 i y} }
      | r = 1 + e^{2 i y}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = i x - i x e^{2 i y}
      | r = 1 + e^{2 i y}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = e^{2 i y} + i x e^{2 i y}
      | r = i x - 1
      | c = rearranging
}}
{{eqn | ll= \leadstoandfrom
      | l = e^{2 i y} \paren {1 + i x }
      | r = i x - 1
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = e^{2 i y}
      | r = \frac {i x - 1} {i x + 1}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = 2 i y
      | r = \map \ln {\dfrac {i x - 1} {i x + 1} }
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = y
      | r = \dfrac 1 {2 i} \map \ln {\dfrac {i x - 1} {i x + 1} }
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = y
      | r = \dfrac i i \times \dfrac 1 {2 i} \map \ln {\dfrac {i x - 1} {i x + 1} }
      | c = multiplying top and bottom by $i$
}}
{{eqn | ll= \leadstoandfrom
      | l = y
      | r = -\dfrac i 2 \map \ln {\dfrac {i x - 1} {i x + 1} }
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of x squared plus a squared/Arccotangent Form

:$\ds \int \frac {\d x} {x^2 + a^2} = -\frac 1 a \arccot \frac x a + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {x^2 + a^2}
      | r = \frac 1 a \int \frac {\d t} {t^2 + 1}
      | c = Substitution of $x \to a t$}}
{{eqn | r = \frac 1 a \int \frac {\d t} {\paren {1 + i t} \paren {1 - i t} }
      | c = factoring
}}
{{eqn | r = \frac 1 {2 a} \paren {\int \frac {\d t} {1 + i t} + \int \frac {\d t} {1 - i t} }
      | c = {{Defof|Partial Fractions Expansion}}
}}
{{eqn | r = \frac 1 {2 a} \paren {i \map \ln {1 - i t} - i \map \ln {1 + i t} } + C
      | c = Primitive of Reciprocal
}}
{{eqn | r = \frac i {2 a} \map \ln {\frac {1 - i t} {1 + i t} } + C
      | c = Sum of Logarithms
}}
{{eqn | r = -\frac i {2 a} \map \ln {\frac {1 + i t} {1 - i t} } + C
      | c = Logarithm of Reciprocal
}}
{{eqn | r = -\frac 1 a \arccot \frac x a + C
      | c = Arccotangent Logarithmic Formulation and substituting back $t \to \dfrac x a$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of x by Root of x squared plus a squared/Reciprocal Logarithm Form

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

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {x \sqrt {x^2 + a^2} }
      | r = -\frac 1 a \map \ln {\frac {a + \sqrt {x^2 + a^2} } x} + C
      | c = Primitive of Reciprocal of $x \sqrt {x^2 + a^2}$: Logarithm form
}}
{{eqn | r = \frac 1 a \map \ln {\frac x {a + \sqrt {a^2 + x^2} } } + C
      | c = Logarithm of Reciprocal
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Hyperbolic Sine

:$\map {\dfrac \d {\d x} } {\sinh x} = \cosh x$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\frac \d {\d x} } {\sinh x}
      | r = \map {\frac \d {\d x} } {\dfrac {e^x - e ^{-x} } 2}
      | c = {{Defof|Hyperbolic Sine}}
}}
{{eqn | r = \frac 1 2 \paren {\map {\frac \d {\d x} } {e^x} - \map {\frac \d {\d x} } {e^{-x} } }
      | c = Linear Combination of Derivatives
}}
{{eqn | r = \frac 1 2 \paren {e^x - \paren {-e^{-x} } }
      | c = Derivative of Exponential Function, Chain Rule for Derivatives
}}
{{eqn | r = \frac {e^x + e^{-x} } 2
      | c = simplification
}}
{{eqn | r = \cosh x
      | c = {{Defof|Hyperbolic Cosine}}
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Hyperbolic Sine

:$\map {\dfrac \d {\d x} } {\sinh x} = \cosh x$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\frac \d {\d x} } {\sinh x}
      | r = \lim_{h \mathop \to 0} \frac {\map \sinh {x + h} - \sinh x} h
      | c = {{Defof|Derivative}}
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {2 \map \cosh {\frac {x + h + x} 2} \map \sinh {\frac {x + h - x} 2} } h
      | c = Hyperbolic Sine minus Hyperbolic Sine
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {2 \map \cosh {x + \frac h 2} \map \sinh {\frac h 2} } h
      | c = 
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {\map \cosh {x + \frac h 2} \map \sinh {\frac h 2} } {\frac h 2}
      | c = 
}}
{{eqn | r = \lim_{2 d \mathop \to 0} \frac {\map \cosh {x + d} \map \sinh d} d
      | c = where $d = \dfrac h 2$
}}
{{eqn | r = \lim_{d \mathop \to 0} \frac {\map \cosh {x + d} \map \sinh d} d
      | c = 
}}
{{eqn | r = \cosh x \lim_{d \mathop \to 0} \frac {\map \sinh d} d
      | c = 
}}
{{eqn | r = \cosh x \lim_{d \mathop \to 0} \frac {e^d - e^{-d} } {2 d}
      | c = {{Defof|Hyperbolic Sine}}
}}
{{eqn | r = \cosh x \lim_{d \mathop \to 0} \frac {e^{2 d} - 1 } {2 d e^d}
      | c = 
}}
{{eqn | r = \cosh x \lim_{d \mathop \to 0} \frac 1 {e^d} \frac {e^{2 d} - 1} {2 d}
      | c = 
}}
{{eqn | r = \cosh x \lim_{d \mathop \to 0} \frac 1 {e^d} \lim_{d \mathop \to 0} \frac {e^{2 d} - 1} {2 d}
      | c = 
}}
{{eqn | r = \cosh x \lim_{d \mathop \to 0} \frac 1 {e^d} \lim_{2 d \mathop \to 0} \frac {e^{2 d} - 1} {2 d}
      | c = 
}}
{{eqn | r = \cosh x \lim_{d \mathop \to 0} \frac 1 {e^d}
      | c = Derivative of Exponential at Zero
}}
{{eqn | r = \cosh x
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Hyperbolic Sine

:$\map {\dfrac \d {\d x} } {\sinh x} = \cosh x$

Proof:
{{begin-eqn}}
{{eqn 	| l = \map {\frac \d {\d x} } {\sinh x}
	| r = -i \map {\frac \d {\d x} } {\sin i x}
	| c = Hyperbolic Sine in terms of Sine 
}}
{{eqn 	| r = \cos i x 
	| c = Derivative of Sine Function 
}}
{{eqn 	| r = \cosh x 
	| c = Hyperbolic Cosine in terms of Cosine 
}}
{{end-eqn}}
{{qed}}
Theorem: Open Ball is Open Set/Metric Space

Let $M = \struct {A, d}$ be a metric space.
Let $x \in A$.
Let $\epsilon \in \R_{>0}$.
Let $\map {B_\epsilon} x$ be an open $\epsilon$-ball of $x$ in $M$.
Then $\map {B_\epsilon} x$ is an open set of $M$.

Proof:
Let $y \in \map {B_\epsilon} x$.
From Open Ball of Point Inside Open Ball, there exists $\delta \in \R_{>0}$ such that:
:$\map {B_\delta} y \subseteq \map {B_\epsilon} x$
The result follows from the definition of open set.
{{qed}}
Theorem: Derivative of Hyperbolic Cosine

:$\map {\dfrac \d {\d x} } {\cosh x} = \sinh x$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\dfrac \d {\d x} } {\cosh x}
      | r = \map {\dfrac \d {\d x} } {\dfrac {e^x + e ^{-x} } 2}
      | c = {{Defof|Hyperbolic Cosine}}
}}
{{eqn | r = \dfrac 1 2 \map {\dfrac \d {\d x} } {e^x + e^{-x} }
      | c = Derivative of Constant Multiple
}}
{{eqn | r = \dfrac 1 2 \paren {e^x + \paren {-e^{-x} } }
      | c = Derivative of Exponential Function, Chain Rule for Derivatives, Linear Combination of Derivatives
}}
{{eqn | r = \dfrac {e^x - e^{-x} } 2
}}
{{eqn | r = \sinh x
      | c = {{Defof|Hyperbolic Sine}}
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Hyperbolic Tangent

:$\map {\dfrac \d {\d x} } {\tanh x} = \sech^2 x = \dfrac 1 {\cosh^2 x}$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\dfrac \d {\d x} } {\tanh x}
      | r = \map {\dfrac \d {\d x} } {\dfrac {\sinh x} {\cosh x} }
      | c = {{Defof|Hyperbolic Tangent|index = 2}}
}}
{{eqn | r = \dfrac {\paren {\dfrac \d {\d x}  \sinh x} \cosh x - \sinh x \paren {\dfrac \d {\d x}  \cosh x} } {\cosh^2 x}
      | c = Quotient Rule for Derivatives
}}
{{eqn | r = \dfrac {\cosh^2 x - \sinh x \paren {\dfrac \d {\d x} \cosh x} } {\cosh^2 x}
      | c = Derivative of Hyperbolic Sine
}}
{{eqn | r = \dfrac {\cosh^2 x - \sinh^2 x} {\cosh^2 x}
      | c = Derivative of Hyperbolic Cosine
}}
{{eqn | r = \dfrac 1 {\cosh^2 x}
      | c = Difference of Squares of Hyperbolic Cosine and Sine
}}
{{eqn | r = \sech^2 x
      | c = {{Defof|Hyperbolic Secant|index = 2}}
}}
{{end-eqn}}
{{qed}}