avewright/proofwiki-math huggingface dataset:
Theorem: Primitive of Hyperbolic Cosecant Function/Hyperbolic Tangent Form

:$\ds \int \csch x \rd x = \ln \size {\tanh \frac x 2} + C$
where $\tanh \dfrac x 2 \ne 0$.

Proof:
{{begin-eqn}}
{{eqn | l = \int \csch x \rd x
      | r = -\ln \size {\csch x + \coth x} + C
      | c = Primitive of $\csch x$: Logarithm Form
}}
{{eqn | r = \ln \size {\frac 1 {\csch x + \coth x} } + C
      | c = Logarithm of Reciprocal
}}
{{eqn | r = \ln \size {\frac 1 {\frac 1 {\sinh x} + \frac {\cosh x} {\sinh x} } } + C
      | c = {{Defof|Hyperbolic Cosecant|index = 2}} and {{Defof|Hyperbolic Cotangent|index = 2}}
}}
{{eqn | r = \ln \size {\frac {\sinh x} {1 + \cosh x} } + C
      | c = 
}}
{{eqn | r = \ln \size {\tanh \frac x 2} + C
      | c = {{Corollary|Half Angle Formula for Hyperbolic Tangent|1}}
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Hyperbolic Cosecant Function/Inverse Hyperbolic Cotangent Form

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

Proof:
Let:
{{begin-eqn}}
{{eqn | l = \int \csch x \rd x
      | r = \int \frac 2 {e^x - e^{-x} } \rd x
      | c = {{Defof|Hyperbolic Cosecant}}
}}
{{eqn | r = \int \frac {2 e^x} {e^{2 x} - 1} \rd x
      | c = multiplying top and bottom by $e^x$
}}
{{end-eqn}}
Let:
{{begin-eqn}}
{{eqn | l = u
      | r = e^x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = u'
      | r = e^x
      | c = Derivative of Exponential Function
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \csch x \rd x
      | r = \int \frac {2 \rd u} {u^2 - 1}
      | c = Integration by Substitution
}}
{{eqn | r = -2 \coth^{-1} u + C
      | c = Primitive of Reciprocal of $x^2 - a^2$: $\coth^{-1}$ form
}}
{{eqn | r = -2 \map {\coth^{-1} } {e^x} + C
      | c = Definition of $u$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Square of Hyperbolic Secant Function

:$\ds \int \sech^2 x \rd x = \tanh x + C$
where $C$ is an arbitrary constant.

Proof:
From Derivative of Hyperbolic Tangent:
:$\map {\dfrac \d {\d x} } {\tanh x} = \sech^2 x$
The result follows from the definition of primitive.
{{Qed}}
Theorem: Primitive of Square of Hyperbolic Cosecant Function

:$\ds \int \csch^2 x \rd x = -\coth x + C$
where $C$ is an arbitrary constant.

Proof:
From Derivative of Hyperbolic Cotangent:
:$\map {\dfrac \d {\d x} } {\coth x} = -\csch^2 x$
The result follows from the definition of primitive.
{{Qed}}
Theorem: Primitive of Square of Hyperbolic Tangent Function

:$\ds \int \tanh^2 x \rd x = x - \tanh x + C$
where $C$ is an arbitrary constant.

Proof:
{{begin-eqn}}
{{eqn | l = \int \tanh^2 x \rd x
      | r = \int \paren {1 - \sech^2 x} \rd x
      | c = Sum of Squares of Hyperbolic Secant and Tangent
}}
{{eqn | r = \int 1 \rd x - \int \sech^2 x \rd x
      | c = Linear Combination of Primitives
}}
{{eqn | r = \int 1 \rd x - \tanh x + C
      | c = Primitive of Square of Hyperbolic Secant Function
}}
{{eqn | r = x - \tanh x + C
      | c = Primitive of Constant
}}
{{end-eqn}}
{{Qed}}
Theorem: Primitive of Square of Hyperbolic Cotangent Function

:$\ds \int \coth^2 x \rd x = x - \coth x + C$
where $C$ is an arbitrary constant.

Proof:
{{begin-eqn}}
{{eqn | l = \int \coth^2 x \rd x
      | r = \int \paren {1 + \csch^2 x} \rd x
      | c = Difference of Squares of Hyperbolic Cotangent and Cosecant
}}
{{eqn | r = \int 1 \rd x + \int \csch^2 x \rd x
      | c = Linear Combination of Primitives
}}
{{eqn | r = \int 1 \rd x - \coth x + C
      | c = Primitive of Square of Hyperbolic Cosecant Function
}}
{{eqn | r = x - \coth x + C
      | c = Primitive of Constant
}}
{{end-eqn}}
{{Qed}}
Theorem: Heaviside Step Function is Piecewise Continuous

Let $c \ge 0$ be a constant real number.
The Heaviside step function:
:$\map {\mu_c} t = \begin {cases} 1 & : t > c \\ 0 & : t < c \end {cases}$
is piecewise continuous for any interval of the form:
:$\closedint {c - M} {c + M}$
where $M > 0$ is some arbitrarily large constant.

Proof:
Let the finite subdivision of $\mu_c$ be:
:$\set {c - M, c, c + M}$
Let $\epsilon > 0$.
For $t \to \paren {c - M}^+$, choose $\delta$ to be any number at all, because:
:$c - M < t < c - M + \delta \implies \size {\map {\mu_c} t - 0} = \size {0 - 0} < \epsilon$
holds, from True Statement is implied by Every Statement.
The case for $t \to c^-$ is proved similarly.
For $t \to c^+$, again, choose $\delta$ to be any number at all, because:
:$c - \delta < t < c \implies \size {\map {\mu_c} t - 1} = \size {1 - 1} < \epsilon$
holds, from True Statement is implied by Every Statement.
The case for $t \to \paren {c + M}^-$ is proved similarly.
For all other $t$, we invoke Continuity of Heaviside Step Function.
{{qed}}
Category:Heaviside Step Function
Category:Continuous Functions
haq21bg4kfx6h8h3jhzxec34b343ckd
Theorem: Euler Formula for Sine Function/Complex Numbers/Proof 1/Lemma 1

The function:
:$\dfrac {\sinh x} x$ 
is increasing for positive real $x$.

Proof:
Let $\map f x = \dfrac {\sinh x} x$.
By Quotient Rule for Derivatives and Derivative of Hyperbolic Sine:
:$\map {f'} x = \dfrac {x \cosh x - \sinh x} {x^2}$
From Hyperbolic Tangent Less than X, we have $\tanh x \le x$ for $x \ge 0$.
Since $\cosh x \ge 0$, we can rearrange to get $x \cosh x - \sinh x \ge 0$.
Since $x^2 \ge 0$, we have $\map {f'} x \ge 0$ for $x \ge 0$.
So by Derivative of Monotone Function it follows that $\map f x$ is increasing for $x \ge 0$.
{{qed}}
Category:Hyperbolic Sine Function
Category:Euler Formula for Sine Function
pj2z8lxqa3jxmucl8rypl8bqmyxs3ss
Theorem: Hyperbolic Tangent Less than X

:$\tanh x \le x$
for $x \ge 0$.

Proof:
Let $\map f x = x - \tanh x$.
By Derivative of Hyperbolic Tangent:
:$\map {f'} x = 1 - \sech^2 x$
Since $\cosh x \ge 1$ for all $x \in \R$, we can deduce that:
:$\map {f'} x \ge 0$
From Derivative of Monotone Function, $\map f x$ is increasing.
By definition of hyperbolic tangent:
:$\map f x = 0$
It follows that $\map f x \ge 0$ for $x \ge 0$.
Hence the result.
{{qed}}
Category:Hyperbolic Tangent Function
ryxjy4bcq7w21sw5ohci51xqz8sts03
Theorem: Primitive of Square of Hyperbolic Sine Function

:$\ds \int \sinh^2 x \rd x = \frac {\sinh 2 x} 4 - \frac x 2 + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \sinh^2 x \rd x
      | r = \int \paren {\frac {\cosh 2 x - 1} 2} \rd x
      | c = Square of Hyperbolic Sine
}}
{{eqn | r = \int \paren {\frac {\cosh 2 x} 2} \rd x - \int \frac 1 2 \rd x
      | c = Linear Combination of Primitives
}}
{{eqn | r = \int \paren {\frac {\cosh 2 x} 2} \rd x - \frac x 2 + C
      | c = Primitive of Constant
}}
{{eqn | r = \frac 1 2 \paren {\frac {\sinh 2 x} 2} - \frac x 2 + C
      | c = Primitive of Function of Constant Multiple and Primitive of Hyperbolic Cosine Function
}}
{{eqn | r = \frac {\sinh 2 x} 4 - \frac x 2 + C
      | c = rearranging
}}
{{end-eqn}}
{{Qed}}
Theorem: Primitive of Square of Hyperbolic Cosine Function

:$\ds \int \cosh^2 x \rd x = \frac {\sinh 2 x} 4 + \frac x 2 + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \cosh^2 x \rd x
      | r = \int \paren {\frac {\cosh 2 x + 1} 2} \rd x
      | c = Square of Hyperbolic Cosine
}}
{{eqn | r = \int \paren {\frac {\cosh 2 x} 2} \rd x + \int \frac 1 2 \rd x
      | c = Linear Combination of Primitives
}}
{{eqn | r = \int \paren {\frac {\cosh 2 x} 2} \rd x + \frac x 2 + C
      | c = Primitive of Constant
}}
{{eqn | r = \frac 1 2 \paren {\frac {\map \sinh {2 x} } 2} + \frac x 2 + C
      | c = Primitive of Function of Constant Multiple and Primitive of Hyperbolic Cosine Function
}}
{{eqn | r = \frac {\sinh 2 x} 4 + \frac x 2 + C
      | c = rearranging
}}
{{end-eqn}}
{{Qed}}
Theorem: Primitive of Product of Hyperbolic Secant and Tangent

:$\ds \int \sech x \tanh x \rd x = -\sech x + C$
where $C$ is an arbitrary constant.

Proof:
From Derivative of Hyperbolic Secant:
:$\dfrac \d {\d x} \sech x = -\sech x \tanh x$
The result follows from the definition of primitive.
{{Qed}}
Theorem: Primitive of Product of Hyperbolic Cosecant and Cotangent

:$\ds \int \csch x \coth x \rd x = -\csch x + C$
where $C$ is an arbitrary constant.

Proof:
From Derivative of Hyperbolic Cosecant:
:$\dfrac \d {\d x} \csch x = -\csch x \coth x$
The result follows from the definition of primitive.
{{Qed}}
Theorem: Primitive of Reciprocal of x squared minus a squared

Let $a \in \R_{>0}$ be a strictly positive real constant.
=== Inverse Hyperbolic Function Form ===
{{:Primitive of Reciprocal of x squared minus a squared/Inverse Hyperbolic Function Form}}
=== $1$st Logarithm Form ===
{{:Primitive of Reciprocal of x squared minus a squared/Logarithm Form 1}}
=== $2$nd Logarithm Form ===
{{:Primitive of Reciprocal of x squared minus a squared/Logarithm Form 2}}

Proof:
Let $\size x > a$.
Let:
{{begin-eqn}}
{{eqn | l = u
      | r = \coth^{-1} {\frac x a}
      | c = {{Defof|Real Inverse Hyperbolic Cotangent}}, which is defined where $\size {\dfrac x a} > 1$
}}
{{eqn | ll= \leadsto
      | l = x
      | r = a \coth u
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d x} {\d u}
      | r = -a \csch^2 u
      | c = Derivative of Hyperbolic Cotangent
}}
{{eqn | ll= \leadsto
      | l = \int \frac 1 {x^2 - a^2} \rd x
      | r = \int \frac {-a \csch^2 u} {a^2 \coth^2 u - a^2} \rd u
      | c = Integration by Substitution
}}
{{eqn | r = -\frac a {a^2} \int \frac {\csch^2 u} {\coth^2 u - 1} \rd u
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = -\frac 1 a \int \frac {\csch^2 u} {\csch^2 u} \rd u
      | c = Difference of Squares of Hyperbolic Cotangent and Cosecant
}}
{{eqn | r = -\frac 1 a \int \rd u
}}
{{eqn | r = -\frac 1 a u + C
      | c = Integral of Constant
}}
{{eqn | r = -\frac 1 a \coth^{-1} {\frac x a} + C
      | c = Definition of $u$
}}
{{end-eqn}}
Theorem: Primitive of Reciprocal of x squared minus a squared

Let $a \in \R_{>0}$ be a strictly positive real constant.
=== Inverse Hyperbolic Function Form ===
{{:Primitive of Reciprocal of x squared minus a squared/Inverse Hyperbolic Function Form}}
=== $1$st Logarithm Form ===
{{:Primitive of Reciprocal of x squared minus a squared/Logarithm Form 1}}
=== $2$nd Logarithm Form ===
{{:Primitive of Reciprocal of x squared minus a squared/Logarithm Form 2}}

Proof:
Let $x > a$.
Then:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {x^2 - a^2}
      | r = -\frac 1 a \arcoth {\frac x a} + C
      | c = Primitive of Reciprocal of $x^2 - a^2$ in $\arcoth$ form
}}
{{eqn | r = -\frac 1 a \paren {\dfrac 1 2 \map \ln {\dfrac {x + a} {x - a} } } + C
      | c = $\arcoth {\dfrac x a}$ in Logarithm Form
}}
{{eqn | r = -\frac 1 {2 a} \map \ln {\frac {x + a} {x - a} } + C
      | c = simplifying
}}
{{eqn | r = \frac 1 {2 a} \map \ln {\frac {x - a} {x + a} } + C
      | c = Logarithm of Reciprocal
}}
{{eqn | r = \frac 1 {2 a} \ln \size {\frac {x - a} {x + a} } + C
      | c = as $\dfrac {x - a} {x + a} > 0$ for $x > a$
}}
{{end-eqn}}
Let $x < -a$.
Let $z = -x$.
Then:
:$\d x = -\d z$
and we then have:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {x^2 - a^2}
      | r = \int \frac {-\d z} {\paren {-z}^2 - a^2}
      | c = Integration by Substitution
}}
{{eqn | r = -\int \frac {\d z} {z^2 - a^2}
      | c = simplifying
}}
{{eqn | r = -\frac 1 {2 a} \map \ln {\frac {z - a} {z + a} } + C
      | c = from above
}}
{{eqn | r = \frac 1 {2 a} \map \ln {\frac {z + a} {z - a} } + C
      | c = Logarithm of Reciprocal
}}
{{eqn | r = \frac 1 {2 a} \map \ln {\frac {-x + a} {-x - a} } + C
      | c = substituting $-x$ back for $z$
}}
{{eqn | r = \frac 1 {2 a} \map \ln {\frac {\size {x - a} } {\size {x + a} } } + C
      | c = as $x < -a$
}}
{{eqn | r = \frac 1 {2 a} \ln \size {\frac {x - a} {x + a} } + C
      | c = 
}}
{{end-eqn}}
The result follows.
{{qed}}
Theorem: Primitive of Reciprocal of x squared minus a squared

Let $a \in \R_{>0}$ be a strictly positive real constant.
=== Inverse Hyperbolic Function Form ===
{{:Primitive of Reciprocal of x squared minus a squared/Inverse Hyperbolic Function Form}}
=== $1$st Logarithm Form ===
{{:Primitive of Reciprocal of x squared minus a squared/Logarithm Form 1}}
=== $2$nd Logarithm Form ===
{{:Primitive of Reciprocal of x squared minus a squared/Logarithm Form 2}}

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {x^2 - a^2}
      | r = \int \frac {\d x} {\paren {x - a} \paren {x + a} }
      | c = Difference of Two Squares
}}
{{eqn | r = \int \frac {\d x} {2 a \paren {x - a} } - \int \frac {\d x} {2 a \paren {x + a} }
      | c = Partial Fraction Expansion
}}
{{eqn | r = \frac 1 {2 a} \int \frac {\d x} {x - a} - \frac 1 {2 a} \int \frac {\d x} {x + a}
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \frac 1 {2 a} \ln \size {x - a} - \frac 1 {2 a} \ln \size {x + a} + C
      | c = Primitive of Reciprocal
}}
{{eqn | r = \dfrac 1 {2 a} \ln \size {\dfrac {x - a} {x + a} } + C
      | c = Difference of Logarithms
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of x squared minus a squared

Let $a \in \R_{>0}$ be a strictly positive real constant.
=== Inverse Hyperbolic Function Form ===
{{:Primitive of Reciprocal of x squared minus a squared/Inverse Hyperbolic Function Form}}
=== $1$st Logarithm Form ===
{{:Primitive of Reciprocal of x squared minus a squared/Logarithm Form 1}}
=== $2$nd Logarithm Form ===
{{:Primitive of Reciprocal of x squared minus a squared/Logarithm Form 2}}

Proof:
From the $1$st logarithm form:
$\quad \ds \int \frac {\d x} {x^2 - a^2} = \begin {cases} \dfrac 1 {2 a} \map \ln {\dfrac {a - x} {a + x} } + C & : \size x < a \\
& \\
\dfrac 1 {2 a} \map \ln {\dfrac {x - a} {x + a} } + C & : \size x > a \\
& \\
\text {undefined} & : \size x = a \end {cases}$
From Primitive of Reciprocal of a squared minus x squared: Logarithm Form: Lemma:
:$\map \ln {\dfrac {x - a} {x + a} }$ is defined {{iff}} $\size x > a$
:$\map \ln {\dfrac {a - x} {a + x} }$ is defined {{iff}} $\size x < a$
Let $\size x > a$.
Then $\map \ln {\dfrac {x - a} {x + a} }$ is defined.
We have that:
{{begin-eqn}}
{{eqn | l = \dfrac {x - a} {x + a}
      | o = >
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {x - a} {x + a}
      | r = \size {\dfrac {x - a} {x + a} }
      | c = 
}}
{{end-eqn}}
So the result holds for $\size x > a$.
Let $\size x < a$.
Then $\map \ln {\dfrac {a - x} {a + x} }$ is defined.
We have:
We have that:
{{begin-eqn}}
{{eqn | l = \dfrac {a - x} {a + x}
      | r = -\dfrac {x - a} {x + a}
      | c = 
}}
{{eqn | o = <
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {a - x} {a + x}
      | r = \size {\dfrac {x - a} {x + a} }
      | c = 
}}
{{end-eqn}}
The result follows.
{{qed}}
Theorem: Primitive of Reciprocal of x squared minus a squared/Logarithm Form 2

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

Proof:
Let $x > a$.
Then:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {x^2 - a^2}
      | r = -\frac 1 a \arcoth {\frac x a} + C
      | c = Primitive of Reciprocal of $x^2 - a^2$ in $\arcoth$ form
}}
{{eqn | r = -\frac 1 a \paren {\dfrac 1 2 \map \ln {\dfrac {x + a} {x - a} } } + C
      | c = $\arcoth {\dfrac x a}$ in Logarithm Form
}}
{{eqn | r = -\frac 1 {2 a} \map \ln {\frac {x + a} {x - a} } + C
      | c = simplifying
}}
{{eqn | r = \frac 1 {2 a} \map \ln {\frac {x - a} {x + a} } + C
      | c = Logarithm of Reciprocal
}}
{{eqn | r = \frac 1 {2 a} \ln \size {\frac {x - a} {x + a} } + C
      | c = as $\dfrac {x - a} {x + a} > 0$ for $x > a$
}}
{{end-eqn}}
Let $x < -a$.
Let $z = -x$.
Then:
:$\d x = -\d z$
and we then have:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {x^2 - a^2}
      | r = \int \frac {-\d z} {\paren {-z}^2 - a^2}
      | c = Integration by Substitution
}}
{{eqn | r = -\int \frac {\d z} {z^2 - a^2}
      | c = simplifying
}}
{{eqn | r = -\frac 1 {2 a} \map \ln {\frac {z - a} {z + a} } + C
      | c = from above
}}
{{eqn | r = \frac 1 {2 a} \map \ln {\frac {z + a} {z - a} } + C
      | c = Logarithm of Reciprocal
}}
{{eqn | r = \frac 1 {2 a} \map \ln {\frac {-x + a} {-x - a} } + C
      | c = substituting $-x$ back for $z$
}}
{{eqn | r = \frac 1 {2 a} \map \ln {\frac {\size {x - a} } {\size {x + a} } } + C
      | c = as $x < -a$
}}
{{eqn | r = \frac 1 {2 a} \ln \size {\frac {x - a} {x + a} } + C
      | c = 
}}
{{end-eqn}}
The result follows.
{{qed}}
Theorem: Primitive of Reciprocal of x squared minus a squared/Logarithm Form 2

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

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {x^2 - a^2}
      | r = \int \frac {\d x} {\paren {x - a} \paren {x + a} }
      | c = Difference of Two Squares
}}
{{eqn | r = \int \frac {\d x} {2 a \paren {x - a} } - \int \frac {\d x} {2 a \paren {x + a} }
      | c = Partial Fraction Expansion
}}
{{eqn | r = \frac 1 {2 a} \int \frac {\d x} {x - a} - \frac 1 {2 a} \int \frac {\d x} {x + a}
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \frac 1 {2 a} \ln \size {x - a} - \frac 1 {2 a} \ln \size {x + a} + C
      | c = Primitive of Reciprocal
}}
{{eqn | r = \dfrac 1 {2 a} \ln \size {\dfrac {x - a} {x + a} } + C
      | c = Difference of Logarithms
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of x squared minus a squared/Logarithm Form 2

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

Proof:
From the $1$st logarithm form:
$\quad \ds \int \frac {\d x} {x^2 - a^2} = \begin {cases} \dfrac 1 {2 a} \map \ln {\dfrac {a - x} {a + x} } + C & : \size x < a \\
& \\
\dfrac 1 {2 a} \map \ln {\dfrac {x - a} {x + a} } + C & : \size x > a \\
& \\
\text {undefined} & : \size x = a \end {cases}$
From Primitive of Reciprocal of a squared minus x squared: Logarithm Form: Lemma:
:$\map \ln {\dfrac {x - a} {x + a} }$ is defined {{iff}} $\size x > a$
:$\map \ln {\dfrac {a - x} {a + x} }$ is defined {{iff}} $\size x < a$
Let $\size x > a$.
Then $\map \ln {\dfrac {x - a} {x + a} }$ is defined.
We have that:
{{begin-eqn}}
{{eqn | l = \dfrac {x - a} {x + a}
      | o = >
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {x - a} {x + a}
      | r = \size {\dfrac {x - a} {x + a} }
      | c = 
}}
{{end-eqn}}
So the result holds for $\size x > a$.
Let $\size x < a$.
Then $\map \ln {\dfrac {a - x} {a + x} }$ is defined.
We have:
We have that:
{{begin-eqn}}
{{eqn | l = \dfrac {a - x} {a + x}
      | r = -\dfrac {x - a} {x + a}
      | c = 
}}
{{eqn | o = <
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {a - x} {a + x}
      | r = \size {\dfrac {x - a} {x + a} }
      | c = 
}}
{{end-eqn}}
The result follows.
{{qed}}
Theorem: Primitive of Reciprocal of a squared minus x squared/Logarithm Form 1

$\quad \ds \int \frac {\d x} {a^2 - x^2} = \begin {cases} \dfrac 1 {2 a} \map \ln {\dfrac {a + x} {a - x} } + C & : \size x < a \\
& \\
\dfrac 1 {2 a} \map \ln {\dfrac {x + a} {x - a} } + C & : \size x > a \\
& \\
\text {undefined} & : \size x = a \end {cases}$

Proof:
=== Case where $\size x < a$ ===
{{:Primitive of Reciprocal of a squared minus x squared/Logarithm Form 1/size of x less than a}}
Theorem: Primitive of Reciprocal of a squared minus x squared/Logarithm Form 1

$\quad \ds \int \frac {\d x} {a^2 - x^2} = \begin {cases} \dfrac 1 {2 a} \map \ln {\dfrac {a + x} {a - x} } + C & : \size x < a \\
& \\
\dfrac 1 {2 a} \map \ln {\dfrac {x + a} {x - a} } + C & : \size x > a \\
& \\
\text {undefined} & : \size x = a \end {cases}$

Proof:
Let $\size x > a$.
Then:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {a^2 - x^2}
      | r = \frac 1 a \arcoth {\frac x a} + C
      | c = Primitive of $\dfrac 1 {a^2 - x^2}$: $\arcoth$ form
}}
{{eqn | r = \frac 1 a \paren {\dfrac 1 2 \map \ln {\dfrac {x + a} {x - a} } } + C
      | c = $\arcoth \dfrac x a$  in Logarithm Form
}}
{{eqn | r = \dfrac 1 {2 a} \map \ln {\frac {x + a} {x - a} } + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of a squared minus x squared/Logarithm Form 1

$\quad \ds \int \frac {\d x} {a^2 - x^2} = \begin {cases} \dfrac 1 {2 a} \map \ln {\dfrac {a + x} {a - x} } + C & : \size x < a \\
& \\
\dfrac 1 {2 a} \map \ln {\dfrac {x + a} {x - a} } + C & : \size x > a \\
& \\
\text {undefined} & : \size x = a \end {cases}$

Proof:
Let $\size x < a$.
Then:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {a^2 - x^2}
      | r = \frac 1 a \artanh {\frac x a} + C
      | c = Primitive of $\dfrac 1 {a^2 - x^2}$: $\artanh$ form
}}
{{eqn | r = \frac 1 a \paren {\dfrac 1 2 \map \ln {\dfrac {a + x} {a - x} } } + C
      | c = $\artanh \dfrac x a$ in Logarithm Form
}}
{{eqn | r = \dfrac 1 {2 a} \map \ln {\dfrac {a + x} {a - x} } + C
      | c = simplifying
}}
{{end-eqn}}
Theorem: Primitive of Reciprocal of a squared minus x squared/Logarithm Form 1

$\quad \ds \int \frac {\d x} {a^2 - x^2} = \begin {cases} \dfrac 1 {2 a} \map \ln {\dfrac {a + x} {a - x} } + C & : \size x < a \\
& \\
\dfrac 1 {2 a} \map \ln {\dfrac {x + a} {x - a} } + C & : \size x > a \\
& \\
\text {undefined} & : \size x = a \end {cases}$

Proof:
Let $\size x < a$.
Then:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {a^2 - x^2}
      | r = \int \frac {\d x} {\paren {a + x} \paren {a - x} }
      | c = Difference of Two Squares
}}
{{eqn | r = \int \frac {\d x} {2 a \paren {a + x} } + \int \frac {\d x} {2 a \paren {a - x} }
      | c = Partial Fraction Expansion
}}
{{eqn | r = \frac 1 {2 a} \int \frac {\d x} {a + x} + \frac 1 {2 a} \int \frac {\d x} {a - x}
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \frac 1 {2 a} \ln \size {a + x} - \frac 1 {2 a} \ln \size {a - x} + C
      | c = Primitive of Reciprocal
}}
{{eqn | r = \frac 1 {2 a} \map \ln {a + x} - \frac 1 {2 a} \map \ln {a - x} + C
      | c = as both $a + x < 0$ and $a - x < 0$
}}
{{eqn | r = \dfrac 1 {2 a} \map \ln {\dfrac {a + x} {a - x} } + C
      | c = Difference of Logarithms
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of a squared minus x squared/Logarithm Form 1

$\quad \ds \int \frac {\d x} {a^2 - x^2} = \begin {cases} \dfrac 1 {2 a} \map \ln {\dfrac {a + x} {a - x} } + C & : \size x < a \\
& \\
\dfrac 1 {2 a} \map \ln {\dfrac {x + a} {x - a} } + C & : \size x > a \\
& \\
\text {undefined} & : \size x = a \end {cases}$

Proof:
Let $\size x < a$.
Then:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {a^2 - x^2}
      | r = -\int \frac {\d x} {x^2 - a^2}
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = -\frac 1 {2 a} \map \ln {\frac {a - x} {a + x} } + C
      | c = Primitive of $\dfrac 1 {x^2 - a^2}$ for $\size x < a$
}}
{{eqn | r = \frac 1 {2 a} \map \ln {\frac {x + a} {x - a} } + C
      | c = Logarithm of Reciprocal
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of a squared minus x squared

Let $a \in \R_{>0}$ be a strictly positive real constant.
=== Inverse Hyperbolic Function Form ===
{{:Primitive of Reciprocal of a squared minus x squared/Inverse Hyperbolic Function Form}}
=== $1$st Logarithm Form ===
{{:Primitive of Reciprocal of a squared minus x squared/Logarithm Form 1}}
=== $2$nd Logarithm Form ===
{{:Primitive of Reciprocal of a squared minus x squared/Logarithm Form 2}}

Proof:
Let $\size x > a$.
Let:
{{begin-eqn}}
{{eqn | l = u
      | r = \coth^{-1} {\frac x a}
      | c = {{Defof|Real Inverse Hyperbolic Cotangent}}, which is defined where $\dfrac x a > 1$
}}
{{eqn | ll=\leadsto
      | l = x
      | r = a \coth u
      | c = 
}}
{{eqn | ll=\leadsto
      | l = \frac {\d x} {\d u}
      | r = -a \csch^2 u
      | c = Derivative of Hyperbolic Cotangent
}}
{{eqn | ll=\leadsto
      | l = \int \frac {\rd x} {a^2 - x^2}
      | r = \int \frac {-a \csch^2 u} {a^2 - a^2 \coth^2 u} \rd u
      | c = Integration by Substitution
}}
{{eqn | r = -\frac a {a^2} \int \frac {\csch^2 u} {-\paren {\coth^2 u - 1} } \rd u
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \frac 1 a \int \frac {\csch^2 u} {\csch^2 u} \rd u
      | c = Difference of Squares of Hyperbolic Cotangent and Cosecant
}}
{{eqn | r = \frac 1 a \int \rd u
}}
{{eqn | r = \frac 1 a u + C
      | c = Integral of Constant
}}
{{eqn | r = \frac 1 a \coth^{-1} \frac x a + C
      | c = Definition of $u$
}}
{{end-eqn}}