avewright/proofwiki-math huggingface dataset:
Theorem: Derivative of Real Area Hyperbolic Cosine of x over a/Corollary 2

:$\map {\dfrac \d {\d x} } {\map \ln {x - \sqrt {x^2 - a^2} } } = -\dfrac 1 {\sqrt {x^2 - a^2} }$
for $x > a$.

Proof:
{{begin-eqn}}
{{eqn | l = -\map {\arcosh} {\frac x a}
      | r = -\map \ln {\frac x a + \sqrt {\paren {\frac x a}^2 - a^2} }
      | c = {{Defof|Real Area Hyperbolic Cosine}}
}}
{{eqn | r = -\map \ln {\frac x a + \dfrac 1 a \sqrt {x^2 - a^2} }
      | c = 
}}
{{eqn | r = -\map \ln {\dfrac 1 a \paren {x + \sqrt {x^2 - a^2} } }
      | c = 
}}
{{eqn | r = -\map \ln {x + \sqrt {x^2 - a^2} } + \ln a
      | c = Difference of Logarithms
}}
{{eqn | r = \map \ln {x - \sqrt {x^2 - a^2} } + \ln a^2 + \ln a
      | c = Negative of Logarithm of x plus Root x squared minus a squared
}}
{{eqn | ll= \leadsto
      | l = \map {\dfrac \d {\d x} } {\map \ln {x - \sqrt {x^2 - a^2} } }
      | r = \map {\dfrac \d {\d x} } {-\map {\cosh^{-1} } {\frac x a} - \ln a^3}
      | c = Sum of Logarithms
}}
{{eqn | r = -\dfrac 1 {\sqrt {x^2 - a^2} } - \map {\dfrac \d {\d x} } {\ln a^3}
      | c = Derivative of Real Area Hyperbolic Cosine of x over a
}}
{{eqn | r = -\dfrac 1 {\sqrt {x^2 - a^2} } + 0
      | c = Derivative of Constant
}}
{{end-eqn}}
When $x = a$ we have that $\sqrt {x^2 - a^2} = 0$ and then $\dfrac 1 {\sqrt {x^2 - a^2} }$ is not defined.
When $\size x < a$ we have that $x^2 - a^2 < 0$ and then $\sqrt {x^2 - a^2}$ is not defined.
When $x < -a$ we have that $x - \sqrt {x^2 - a^2} < 0$ and so $\map \ln {x + \sqrt {x^2 - a^2} }$ is not defined.
Hence the restriction on the domain.
{{qed}}
Theorem: Primitive of Reciprocal of Root of x squared minus a squared/Logarithm Form/Corollary

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

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {\sqrt {x^2 - a^2} }
      | r = \ln \size {x + \sqrt {x^2 - a^2} } + C
      | c = Primitive of $\dfrac 1 {\sqrt {x^2 - a^2} }$ in Logarithm Form
}}
{{eqn | l = \int \frac {\d x} {-\sqrt {x^2 + a^2} }
      | r = -\ln \size {x + \sqrt {x^2 - a^2} } + C
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \ln \size {x - \sqrt {x^2 - a^2} } + C + \map \ln {a^2}
      | c = Negative of Logarithm of x plus Root x squared minus a squared
}}
{{eqn | r = \ln \size {x - \sqrt {x^2 - a^2} } + C
      | c = subsuming $\map \ln {a^2}$ into the constant
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Real Area Hyperbolic Tangent of x over a/Corollary

:$\map {\dfrac \d {\d x} } {\dfrac 1 {2 a} \map \ln {\dfrac {a + x} {a - x} } } = \dfrac 1 {a^2 - x^2}$
where $\size x < a$.

Proof:
{{begin-eqn}}
{{eqn | l = \dfrac 1 a \map {\tanh^{-1} } {\frac x a}
      | r = \dfrac 1 a \cdot \dfrac 1 2 \map \ln {\dfrac {1 + \frac x a} {1 - \frac x a} }
      | c = {{Defof|Real Area Hyperbolic Tangent}}
}}
{{eqn | r = \dfrac 1 {2 a} \map \ln {\dfrac {a + x} {a - x} }
      | c = multiplying top and bottom of argument by $a$
}}
{{eqn | ll= \leadsto
      | l = \map {\dfrac \d {\d x} } {\dfrac 1 {2 a} \map \ln {\dfrac {a + x} {a - x} } }
      | r = \map {\dfrac \d {\d x} } {\dfrac 1 a \map {\tanh^{-1} } {\frac x a} }
      | c = 
}}
{{eqn | r = \dfrac 1 a \cdot \dfrac a {a^2 - x^2}
      | c = Derivative of Real Area Hyperbolic Tangent of x over a
}}
{{eqn | r = \dfrac 1 {a^2 - x^2}
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Real Area Hyperbolic Cotangent of x over a/Corollary

:$\map {\dfrac \d {\d x} } {\dfrac 1 {2 a} \map \ln {\dfrac {x + a} {x - a} } } = \dfrac 1 {a^2 - x^2}$
where $\size x > a$.

Proof:
{{begin-eqn}}
{{eqn | l = \dfrac 1 a \map \arcoth {\frac x a}
      | r = \dfrac 1 a \cdot \dfrac 1 2 \map \ln {\dfrac {\frac x a + 1} {\frac x a - 1} }
      | c = {{Defof|Real Area Hyperbolic Cotangent}}
}}
{{eqn | r = \dfrac 1 {2 a} \map \ln {\dfrac {x + a} {x - a} }
      | c = multiplying top and bottom of argument by $a$
}}
{{eqn | ll= \leadsto
      | l = \map {\dfrac \d {\d x} } {\dfrac 1 {2 a} \map \ln {\dfrac {x + a} {x - a} } }
      | r = \map {\dfrac \d {\d x} } {\dfrac 1 a \map \arcoth {\frac x a} }
      | c = 
}}
{{eqn | r = \dfrac 1 a \cdot \dfrac {-a} {x^2 - a^2}
      | c = Derivative of Real Area Hyperbolic Cotangent of x over a
}}
{{eqn | r = \dfrac 1 {a^2 - x^2}
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Rank of Matroid Circuit is One Less Than Cardinality/Lemma

:$C \setminus \set x$ is a maximal independent subset of $C$

Proof:
From Set Difference is Subset:
:$C \setminus \set x \subseteq C$
Because $x \in C$ and $x \notin C \setminus \set x$:
:$C \setminus \set x \ne C$
From Proper Subset of Matroid Circuit is Independent and matroid axiom $(\text I 1)$:
:$C \setminus \set x \in \mathscr I$
Let $X$ be an independent subset such that:
:$C \setminus \set x \subseteq X \subseteq C$
As $C$ is dependent:
:$X \ne C$
{{AimForCont}}:
:$x \in X$
From Singleton of Element is Subset:
:$\set x \subseteq X$
:$\set x \subseteq C$
We have:
{{begin-eqn}}
{{eqn | l = X
      | r = X \cup \set x
      | c = Union with Superset is Superset
}}
{{eqn | o = \supseteq
      | r = \paren{C \setminus \set x} \cup \set x
      | c = Set Difference over Subset
}}
{{eqn | r = C \cup \set x
      | c = Set Difference with Union
}}
{{eqn | r = C
      | c = Union with Superset is Superset
}}
{{end-eqn}}
Hence $C = X$ by definition of set equality. 
This contradicts the fact that:
:$X \ne C$
Hence:
:$x \notin X$
From Intersection With Singleton is Disjoint if Not Element:
:$X \cap \set x = \O$
We have:
{{begin-eqn}}
{{eqn | l = X
      | r = X \setminus \set x
      | c = Set Difference with Disjoint Set
}}
{{eqn | o = \subseteq
      | r = C \setminus \set x
      | c = Set Difference over Subset
}}
{{end-eqn}}
By definition of set equality:
:$X = C \setminus \set x$ 
It follows that $C \setminus \set x$ is a maximal independent subset of $C$ by definition.
{{qed}}
Category:Rank of Matroid Circuit is One Less Than Cardinality
adw1lr8n677ep7vvcw9p3mhjlb7ga7r
Theorem: Union of Matroid Base with Element of Complement is Dependent

:$B \cup \set x$ is a dependent superset of $B$

Proof:
From Set is Subset of Union:
:$B \subseteq B \cup \set x$
Because $x \in B \cup \set x$ and $x \notin B$:
:$B \ne B \cup \set x$
Hence:
:$B \subsetneq B \cup \set x$
By definition of base:
:$B$ is a maximal independent subset
Hence:
:$B \cup \set x \notin \mathscr I$
{{qed}}
Category:Matroid Bases
Category:Matroid Dependent Subsets
hqyocl37nhqqebtsc34rmmdk54pukxn
Theorem: Primitive of Power of a x + b/Proof 1

{{:Primitive of Power of a x + b}}
where $n \ne 1$.

Proof:
Let $u = a x + b$.
Then:
{{begin-eqn}}
{{eqn | l = \int \paren {a x + b}^n \rd x
      | r = \frac 1 a \int u^n \rd u
      | c = Primitive of Function of $a x + b$
}}
{{eqn | r = \frac 1 a \frac {u^{n + 1} } {n + 1} + C
      | c = Primitive of Power
}}
{{eqn | r = \frac {\paren {a x + b}^{n + 1} } {\paren {n + 1} a} + C
      | c = substituting for $u$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power of a x + b/Proof 2

{{:Primitive of Power of a x + b}}
where $n \ne 1$.

Proof:
Let $u = a x + b$.
Then:
:$\dfrac {\d u} {\d x} = a$
Then:
{{begin-eqn}}
{{eqn | l = \int \paren {a x + b}^n \rd x
      | r = \int \dfrac {u^n} a \rd u
      | c = Integration by Substitution
}}
{{eqn | r = \dfrac 1 a \dfrac {u^{n + 1} } {n + 1}
      | c = Primitive of Power
}}
{{eqn | r = \frac {\paren {a x + b}^{n + 1} } {\paren {n + 1} a} + C
      | c = substituting back for $u$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of a squared minus x squared/Inverse Hyperbolic Function Form

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

Proof:
First note that if $x = a$ then $a^2 - x^2 = 0$ and so $\dfrac 1 {a^2 - x^2}$ is undefined.
Theorem: Primitive of Reciprocal of a squared minus x squared/Inverse Hyperbolic Cotangent Form

:$\ds \int \frac {\d x} {a^2 - x^2} = \frac 1 a \coth^{-1} \frac x a + C$
where $\size x > a$.

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}}
Theorem: Primitive of Reciprocal of a squared minus x squared/Logarithm Form 1/size of x less than a

Let $\size x < a$.
Then:
:$\ds \int \frac {\d x} {a^2 - x^2} = \dfrac 1 {2 a} \map \ln {\dfrac {a + x} {a - x} } + C$

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/size of x less than a

Let $\size x < a$.
Then:
:$\ds \int \frac {\d x} {a^2 - x^2} = \dfrac 1 {2 a} \map \ln {\dfrac {a + x} {a - x} } + C$

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/size of x less than a

Let $\size x < a$.
Then:
:$\ds \int \frac {\d x} {a^2 - x^2} = \dfrac 1 {2 a} \map \ln {\dfrac {a + x} {a - x} } + C$

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/Logarithm Form 1/size of x greater than a

Let $\size x > a$.
Then:
:$\ds \int \frac {\d x} {a^2 - x^2} = \dfrac 1 {2 a} \map \ln {\dfrac {x + a} {x - a} } + C$

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

Let $a \in \R_{>0}$ be a strictly positive real constant.
Let $x \in \R$ such that $\size x \ne a$.

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

Let $a \in \R_{>0}$ be a strictly positive real constant.
Let $x \in \R$ such that $\size x \ne a$.

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

Let $a \in \R_{>0}$ be a strictly positive real constant.
Let $x \in \R$ such that $\size x \ne a$.

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

Let $a \in \R_{>0}$ be a strictly positive real constant.
Let $x \in \R$ such that $\size x \ne a$.

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/Logarithm Form 2

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

Proof:
From the $1$st logarithm form:
:$\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}$
From Primitive of Reciprocal of a squared minus x squared: Logarithm Form: Lemma:
:$\map \ln {\dfrac {a + x} {a - x} }$ is defined {{iff}} $\size x < a$
:$\map \ln {\dfrac {x + a} {x - a} }$ is defined {{iff}} $\size x > a$
Let $\size x < a$.
Then $\map \ln {\dfrac {a + x} {a - x} }$ is defined.
We have that:
{{begin-eqn}}
{{eqn | l = \dfrac {a + x} {a - x}
      | o = >
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {a + x} {a - x}
      | r = \size {\dfrac {a + x} {a - x} }
      | c = 
}}
{{end-eqn}}
So the result holds for $\size x < a$.
Let $\size x > a$.
Then $\map \ln {\dfrac {x + a} {x - a} }$ is defined.
We have:
We have that:
{{begin-eqn}}
{{eqn | l = \dfrac {x + a} {x - a}
      | r = -\dfrac {a + x} {a - x}
      | c = 
}}
{{eqn | o = <
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {x + a} {x - a}
      | r = \size {\dfrac {a + x} {a - x} }
      | c = 
}}
{{end-eqn}}
The result follows.
{{qed}}
Theorem: Primitive of Reciprocal of x squared minus a squared/Logarithm Form

Let $a \in \R_{>0}$ be a strictly positive real constant.
Let $x \in \R$ such that $\size x \ne a$.
=== $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/Logarithm Form

Let $a \in \R_{>0}$ be a strictly positive real constant.
Let $x \in \R$ such that $\size x \ne a$.
=== $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/Logarithm Form

Let $a \in \R_{>0}$ be a strictly positive real constant.
Let $x \in \R$ such that $\size x \ne a$.
=== $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/Inverse Hyperbolic Function Form

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

Proof:
First note that if $x = a$ then $a^2 - x^2 = 0$ and so $\dfrac 1 {x^2 - a^2}$ is undefined.
Theorem: Primitive of Reciprocal of x squared minus a squared/Logarithm Form 1

$\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}$

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

Let $\size x < a$.
Then:
:$\ds \int \frac {\d x} {x^2 - a^2} = \dfrac 1 {2 a} \map \ln {\dfrac {a - x} {a + x} } + C$

Proof:
Let $\size x < a$.
Then:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {x^2 - a^2}
      | r = -\frac 1 a \artanh {\frac x a} + C
      | c = Primitive of $\dfrac 1 {x^2 - a^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
}}
{{eqn | r = \dfrac 1 {2 a} \map \ln {\dfrac {a - x} {a + x} } + C
      | c = Logarithm of Reciprocal
}}
{{end-eqn}}
Theorem: Primitive of Reciprocal of x squared minus a squared/Logarithm Form 1/size of x greater than a

Let $\size x > a$.
Then:
:$\ds \int \frac {\d x} {x^2 - a^2} = \dfrac 1 {2 a} \map \ln {\dfrac {x - a} {x + a} } + C$

Proof:
Let $\size 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 $\dfrac 1 {x^2 - a^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
}}
{{eqn | r = \dfrac 1 {2 a} \map \ln {\frac {x - a} {x + a} } + C
      | c = Reciprocal of Logarithm
}}
{{end-eqn}}
{{qed}}
Theorem: Power Set is Closed under Complement

Let $S$ be a set.
Let $\powerset S$ be the power set of $S$.
Then:
:$\forall A \in \powerset S: \relcomp S A \in \powerset S$
where $\relcomp S A$ denotes the complement of $A$ relative to $S$.

Proof:
{{begin-eqn}}
{{eqn | l = A
      | o = \in
      | r = \powerset S
      | c = 
}}
{{eqn | ll= \leadsto
      | l = A
      | o = \subseteq
      | r = S
      | c = {{Defof|Power Set}}
}}
{{eqn | ll= \leadsto
      | l = S \setminus A
      | o = \subseteq
      | r = S
      | c = Set Difference is Subset
}}
{{eqn | ll= \leadsto
      | l = \relcomp S A
      | o = \subseteq
      | r = S
      | c = {{Defof|Relative Complement}}
}}
{{eqn | ll= \leadsto
      | l = \relcomp S A
      | o = \in
      | r = \powerset S
      | c = {{Defof|Power Set}}
}}
{{end-eqn}}
{{qed}}