avewright/proofwiki-math huggingface dataset:
Theorem: Field Product with Non-Zero Element yields Unique Solution

Let $\struct {F, +, \times}$ be a field whose zero is $0_F$ and whose unity is $1_F$.
Let $a, b, x \in F$ such that $b \ne 0_F$.
Let:
:$b \times x = a$
Then:
:$x = a b^{-1}$
That is:
:$x = \dfrac a b$
where $\dfrac a b$ denotes division.

Proof:
{{begin-eqn}}
{{eqn | l = b \times x
      | r = a
      | c = with $b \ne 0_F$
}}
{{eqn | ll= \leadsto
      | l = b^{-1} \times \paren {b \times x}
      | r = b^{-1} \times a
      | c = multiplying both sides by $b^{-1}$, which exists because $b \ne 0$
}}
{{eqn | ll= \leadsto
      | l = \paren {b^{-1} \times b} \times x
      | r = b^{-1} \times a
      | c = {{Field-axiom|M1}}
}}
{{eqn | ll= \leadsto
      | l = 1_F \times x
      | r = b^{-1} \times a
      | c = {{Field-axiom|M4}}
}}
{{eqn | ll= \leadsto
      | l = x
      | r = b^{-1} \times a
      | c = {{Field-axiom|M3}}
}}
{{end-eqn}}
{{qed}}
Theorem: Field Unity Divided by Element equals Multiplicative Inverse

Let $\struct {F, +, \times}$ be a field whose zero is $0_F$ and whose unity is $1_F$.
Let $a \in F$.
Then:
:$\dfrac {1_F} a = a^{-1}$
where $\dfrac {1_F} a$ denotes division.

Proof:
{{begin-eqn}}
{{eqn | l = \dfrac {1_F} a
      | r = 1_F \times a^{-1}
      | c = {{Defof|Division over Field}}
}}
{{eqn | r = a^{-1} \times 1_F
      | c = {{Field-axiom|M2}}
}}
{{eqn | r = a^{-1}
      | c = {{Field-axiom|M3}}
}}
{{end-eqn}}
{{qed}}
Theorem: Cancellation Law for Field Product

Let $\struct {F, +, \times}$ be a field whose zero is $0_F$ and whose unity is $1_F$.
Let $a, b, c \in F$.
Then:
:$a \times b = a \times c \implies a = 0_F \text { or } b = c$

Proof:
Let $a \times b = a \times c$.
Then:
{{begin-eqn}}
{{eqn | l = a
      | o = \ne
      | r = 0_F
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists a^{-1} \in F
      | l = a^{-1} \times a
      | r = 1_F
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a^{-1} \times \paren {a \times b}
      | r = a^{-1} \times \paren {a \times c}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {a^{-1} \times a} \times b
      | r = \paren {a^{-1} \times a} \times c
      | c = {{Field-axiom|M1}}
}}
{{eqn | ll= \leadsto
      | l = 1_F \times b
      | r = 1_F \times c
      | c = {{Field-axiom|M4}}
}}
{{eqn | ll= \leadsto
      | l = b
      | r = c
      | c = {{Field-axiom|M3}}
}}
{{end-eqn}}
That is:
:$a \ne 0 \implies b = c$
{{qed|lemma}}
Suppose $b \ne c$.
Then by Rule of Transposition:
:$\map \neg {a \ne 0}$
that is:
:$a = 0_F$
and we note that in this case:
:$a \times b = 0_F = a \times c$
{{qed}}
Theorem: Inverse of Field Product

Let $\struct {F, +, \times}$ be a field whose zero is $0_F$ and whose unity is $1_F$.
Let $a, b \in F$ such that $a \ne 0$ and $b \ne 0$.
Then:
:$\paren {a \times b}^{-1} = b^{-1} \times a^{-1}$

Proof:
We are given that $a \ne 0$ and $b \ne 0$.
From Field has no Proper Zero Divisors and Rule of Transposition, we have:
:$a \times b \ne 0$
By {{Field-axiom|M4}} we have that $\paren {a \times b}^{-1}$ exists.
Then we have:
{{begin-eqn}}
{{eqn | l = \paren {b^{-1} \times a^{-1} } \times \paren {a \times b}
      | r = b^{-1} \times \paren {a^{-1} \times a} \times b
      | c = {{Field-axiom|M1}}
}}
{{eqn | r = b^{-1} \times 1_F \times b
      | c = {{Field-axiom|M4}}
}}
{{eqn | r = b^{-1} \times b
      | c = {{Field-axiom|M3}}
}}
{{eqn | r = 1_F
      | c = {{Field-axiom|M4}}
}}
{{end-eqn}}
Hence the result by definition of multiplicative inverse.
{{qed}}
Theorem: Inverse of Field Product

Let $\struct {F, +, \times}$ be a field whose zero is $0_F$ and whose unity is $1_F$.
Let $a, b \in F$ such that $a \ne 0$ and $b \ne 0$.
Then:
:$\paren {a \times b}^{-1} = b^{-1} \times a^{-1}$

Proof:
By definition, a field is a non-trivial division ring whose ring product is commutative.
By definition, a division ring is a ring with unity such that every non-zero element is a unit. 
Hence we can use Inverse of Division Product:
:$\paren {\dfrac a b}^{-1} = \dfrac {1_R} {\paren {a / b}} = \dfrac b a$
which applies to the group of units of a comutative ring with unity.
{{qed}}
Theorem: Set Difference of Larger Set with Smaller is Not Empty

Let $S$ and $T$ be finite sets.
Let $\card S > \card T$.
Then:
:$S \setminus T \ne \O$

Proof:
From Cardinality of Subset of Finite Set:
:$S \nsubseteq T$
From the contrapositive statement of Set Difference with Superset is Empty Set:
:$S \setminus T \ne \O$.
{{qed}}
Category:Set Difference
Category:Cardinality
n3frdoief51ck6ehmgy4zv0wz97nrbu
Theorem: Autocovariance Matrix for Stationary Process is Variance by Autocorrelation Matrix

Let $S$ be a strictly stationary stochastic process giving rise to a time series $T$.
Let $\sequence {s_n}$ be a sequence of $n$ successive values of $T$:
:$\sequence {s_n} = \tuple {z_1, z_2, \dotsb, z_n}$
Let $\boldsymbol \Gamma_n$ denote the '''autocovariance matrix''' associated with $S$ for $\sequence {s_n}$.
Let $\mathbf P_n$ denote the '''autocorrelation matrix''' associated with $S$ for $\sequence {s_n}$.
Then:
:$\boldsymbol \Gamma_n = \sigma_z^2 \mathbf P_n$
where $\sigma_z^2$ denotes the variance of $S$.

Proof:
From Autocorrelation of Strictly Stationary Stochastic Process:
:$\rho_k = \dfrac {\gamma_k} {\gamma_0}$
Then from Autocovariance at Zero Lag for Strictly Stationary Stochastic Process is Variance:
:$\gamma_0 = \sigma_z^2$
Hence:
:$\gamma_k = \sigma_z^2 \rho_k$
and the result follows.
{{qed}}
Theorem: Determinant of Autocorrelation Matrix is Strictly Positive

Let $S$ be a strictly stationary stochastic process giving rise to a time series $T$.
Let $\sequence {s_n}$ be a sequence of $n$ successive values of $T$:
:$\sequence {s_n} = \tuple {z_1, z_2, \dotsb, z_n}$
Let $\mathbf P_n$ denote the '''autocorrelation matrix''' associated with $S$ for $\sequence {s_n}$.
The determinant of $\mathbf P_n$ is strictly positive.

Proof:
We have that the Autocorrelation Matrix is Positive Definite.
The result follows from Determinant of Positive Definite Matrix is Strictly Positive.
{{qed}}
Theorem: Sum of Wholly Real Numbers is Wholly Real

Let $x = \tuple {a, 0}$ and $y = \tuple {b, 0}$ be wholly real complex numbers.
Then $x + y$ is also wholly real.

Proof:
We have:
{{begin-eqn}}
{{eqn | l = x + y
      | r = \tuple {a, 0} + \tuple {b, 0}
      | c = 
}}
{{eqn | r = \tuple {a + b, 0 + 0}
      | c = {{Defof|Complex Addition}}
}}
{{eqn | r = \tuple {a + b, 0}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Product of Wholly Real Numbers is Wholly Real

Let $x = \tuple {a, 0}$ and $y = \tuple {b, 0}$ be wholly real complex numbers.
Then $x y$ is also wholly real.

Proof:
We have:
{{begin-eqn}}
{{eqn | l = x y
      | r = \tuple {a, 0} \tuple {b, 0}
      | c = 
}}
{{eqn | r = \tuple {a \times b - 0 \times 0, a \times 0 + 0 \times b}
      | c = {{Defof|Complex Multiplication}}
}}
{{eqn | r = \tuple {a \times b, 0}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Product of Imaginary Unit with Itself

Let $\tuple {0, 1}$ denote the imaginary unit.
Then:
:$\tuple {0, 1} \times \tuple {0, 1} = \tuple {-1, 0}$
where $\times$ denotes complex multiplication.

Proof:
{{begin-eqn}}
{{eqn | l = \tuple {0, 1} \times \tuple {0, 1}
      | r = \tuple {0 \times 0 - 1 \times 1, 0 \times 1 + 0 \times 1}
      | c = {{Defof|Complex Multiplication}}
}}
{{eqn | r = \tuple {-1, 0}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Element of Matroid Base and Circuit has Substitute

Let $M = \struct {S, \mathscr I}$ be a matroid.
Let $B \subseteq S$ be a base of $M$.
Let $C \subseteq S$ be a circuit of $M$.
Let $x \in B \cap C$.
Then:
:$\exists y \in C \setminus B : \paren{B \setminus \set x} \cup \set y$ is a base of $M$
That is, there exists $y \in C \setminus B$ such that substituting $y$ for $x$ in $B$ is another base.

Proof:
By definition of a circuit we have:
Theorem: Set Difference with Non-Empty Proper Subset is Non-Empty Proper Subset

Let $S$ be a set.
Let $T \subsetneq S$ be a non-empty proper subset of $S$.
Let $S \setminus T$ denote the set difference between $S$ and $T$.
Then:
:$S \setminus T$ is a non-empty proper subset of $S$

Proof:
From Set Difference is Subset:
:$S \setminus T \subseteq S$
From Set Difference with Proper Subset:
:$S \setminus T \ne \O$
Then {{hypothesis}}:
:$T \ne \O$
From Intersection with Subset is Subset:
:$S \cap T = T$
Hence:
:$S \cap T \ne \O$
From the contrapositive statement of Set Difference with Disjoint Set:
:$S \setminus T \ne S$
It follows that $S \setminus T$ is a non-empty proper subset by definition.
{{qed}}
Category:Set Difference
Category:Proper Subsets
rzlunjl5xlaqshqzjwnc8ym4rhkhcu4
Theorem: Subspace of Normed Vector Space with Induced Norm forms Normed Vector Space

Let $\struct {X, \norm {\, \cdot \,}_X}$ be a normed vector space.
Let $Y \subseteq X$ be a vector subspace.
Let $\norm {\, \cdot \,}_Y$ be the induced norm on $Y$.
Then $\struct {Y, \norm {\, \cdot \,}_Y}$ is a normed vector space.

Proof:
=== Positive definiteness ===
By definition of induced norm:
:$\forall y \in Y : \norm {y}_Y = \norm {y}_X > 0$
Suppose $y \in Y: \norm y_Y = 0$.
Since $\norm {\, \cdot \,}_Y$ is an induced norm in $\struct {X, \norm {\, \cdot \,}_X}$:
:$\norm y_X = 0$
Therefore:
:$y = \mathbf 0 \in X$
By definition of a vector subspace, $Y$ satisfies {{Abelian-group-axiom|2||underlying}}:
:$\mathbf 0 \in Y$
Thus:
:$y = \mathbf 0 \in Y \subseteq X$
Theorem: All Bases of Matroid have same Cardinality/Corollary

Let $X \subseteq S$ be any independent subset of $M$.
Then:
:$\card X \le \card B$

Proof:
From Independent Subset is Contained in Maximal Independent Subset :
:$\exists B' \subseteq S : X \subseteq B'$ and $B'$ is a maximal independent subset of $S$
By definition of a base:
:$B'$ is a base of $M$
From Cardinality of Subset of Finite Set:
:$\card X \le \card {B'}$
From All Bases of Matroid have same Cardinality:
:$\card{B'} = \card B$
Hence:
:$\card X \le \card B$
{{qed}}
Category:Matroid Bases
sd9e8akqbeudh2s2ptqx2vwt39dsz88
Theorem: Independent Set can be Augmented by Larger Independent Set/Corollary

Let $B \subseteq S$ be a base of $M$.
Then:
:$\exists Z \subseteq B \setminus X : \card{X \cup Z} = \card B  : X \cup Z$ is a base of $M$

Proof:
From Cardinality of Independent Set of Matroid is Smaller or Equal to Base:
:$\card X \le \card B$
Theorem: Independent Subset is Base if Cardinality Equals Rank of Matroid/Corollary

Let $B \subseteq S$ be a base of $M$.
Let $X \subseteq S$ be any independent subset of $M$.
Let $\card X = \card B$.
Then:
:$X$ is a base of $M$.

Proof:
From All Bases of Matroid have same Cardinality:
:$\card B = \map \rho S$
where $\rho$ denotes the rank function on $M$.
Hence:
:$\card X = \map \rho S$
From Independent Subset is Base if Cardinality Equals Rank of Matroid:
:$X$ is a base of $M$.
{{qed}}
Category:Matroid Independent Subsets
Category:Matroid Bases
8o2nhppqpqx3eulh6z8gke4b6k7rhtu
Theorem: Matroid Unique Circuit Property

Let $M = \struct {S, \mathscr I}$ be a matroid.
Let $X \subseteq S$ be an independent subset of $M$.
Let $x \in S$ such that:
:$X \cup \set x$ is a dependent subset of $M$.
Then there exists a unique circuit $C$ such that:
:$x \in C \subseteq X \cup \set x$

Proof:
From Dependent Subset Contains a Circuit:
:there exists a circuit $C$ such that $C \subseteq X \cup \set x$
From Dependent Subset of Independent Set Union Singleton Contains Singleton:
:$x \in C$
{{AimForCont}} $C'$ is circuit of $M$ such that:
:$C' \ne C$
:$C' \subseteq X \cup \set x$
From Dependent Subset of Independent Set Union Singleton Contains Singleton:
:$x \in C'$
Hence:
:$x \in C \cap C'$
From Circuits of Matroid iff Matroid Circuit Axioms, the set $\mathscr C$ of all circuits satisfies the matroid circuit axiom $(\text C 3)$:
{{begin-axiom}}
{{axiom | n = \text C 3
        | q = \forall C_1, C_2 \in \mathscr C
        | mr = C_1 \ne C_2 \land z \in C_1 \cap C_2 \implies \exists C_3 \in \mathscr C : C_3 \subseteq \paren {C_1 \cup C_2} \setminus \set z
}}
{{end-axiom}}
Hence there exists a circuit $C_3$ of $M$:
:$C_3 \subseteq \paren{C \cup C'} \setminus \set x \subseteq X$
This contradicts the independence of $X$.
The result follows.
{{qed}}
Theorem: Matroid Unique Circuit Property

Let $M = \struct {S, \mathscr I}$ be a matroid.
Let $X \subseteq S$ be an independent subset of $M$.
Let $x \in S$ such that:
:$X \cup \set x$ is a dependent subset of $M$.
Then there exists a unique circuit $C$ such that:
:$x \in C \subseteq X \cup \set x$

Proof:
From Dependent Subset Contains a Circuit:
:there exists a circuit $C$ such that $C \subseteq X \cup \set x$
From Dependent Subset of Independent Set Union Singleton Contains Singleton:
:$x \in C$
{{AimForCont}} $C'$ is circuit of $M$ such that:
:$C' \ne C$
:$C' \subseteq X \cup \set x$
From Dependent Subset of Independent Set Union Singleton Contains Singleton:
:$x \in C'$
By the definition of minimal dependent subset:
:$C \nsubseteq C'$
By the definition of a subset:
:$\exists y \in C \setminus C'$
By the definition of minimal dependent subset:
:$C \setminus \set y \in \mathscr I$
From Independent Subset is Contained in Maximal Independent Subset:
:$\exists Y \in \mathscr I : C \setminus \set y \subseteq Y \subseteq X \cup \set x : Y$ is a maximal independent subset of $X \cup \set x$
By assumption:
:$X$ is a maximal independent subset of $X \cup \set x$
By matroid axiom $(\text I 6)$:
:$\card Y = \card X$
As $x \in C'$ and $y \notin C'$ then:
:$x \ne y$
Hence:
:$x \in C \setminus \set y$
By matroid axiom $(\text I 2)$:
:$C \setminus \set y \cup \set y = C \nsubseteq Y$ 
Hence:
:$y \notin Y$
Hence:
:$Y \subseteq \paren {X \cup \set x} \setminus \set y$
From Cardinality of Subset of Finite Set:
:$\card Y \le \card {\paren {X \cup \set x} \setminus \set y}$
We have:
{{begin-eqn}}
{{eqn | l = \card {\paren {X \cup \set x} \setminus \set y}
      | r = \card {\paren {X \cup \set x} } - \card {\set y}
      | c =
}}
{{eqn | r = \card X + \card {\set x} - \card {\set y}
      | c =
}}
{{eqn | r = \card X + 1 - 1
      | c =
}}
{{eqn | r = \card X
      | c =
}}
{{eqn | r = \card Y
      | c =
}}
{{end-eqn}}
From Cardinality of Proper Subset of Finite Set:
:$Y = \paren {X \cup \set x} \setminus \set y$
Hence:
:$\paren {X \cup \set x} \setminus \set y \in \mathscr I$
As $y \notin C'$ and $C' \subseteq X \cup \set x$ then:
:$C' \subseteq \paren {X \cup \set x} \setminus \set y$
From Superset of Dependent Set is Dependent:
:$\paren {X \cup \set x} \setminus \set y \notin \mathscr I$
This contradicts the previous statement that 
:$\paren {X \cup \set x} \setminus \set y \in \mathscr I$
It follows that $C$ is the unique circuit such that:
:$C \subseteq X \cup \set x$
{{qed}}
Theorem: Absolute Value of Negative

Let $x \in \R$ be a real number.
Then:
:$\size x = \size {-x}$
where $\size x$ denotes the absolute value of $x$.

Proof:
Let $x \ge 0$.
By definition of absolute value:
:$\size x = x$
We have that:
:$-x < 0$
and so by definition of absolute value:
:$\size {-x} = -\paren {-x} = x$
{{qed|lemma}}
Now let $x < 0$.
By definition of absolute value:
:$\size x = -x$
We have that:
:$-x > 0$
and so by definition of absolute value:
:$\size {-x} = -x$
{{qed|lemma}}
In both cases it is seen that:
:$\size x = \size {-x}$
{{qed}}
Category:Absolute Value Function
t37uhmiwnd2f7d2f96l2zegyz2peqsr
Theorem: Dependent Subset Contains a Circuit

Let $M = \struct {S, \mathscr I}$ be a matroid.
Let $\mathscr C$ denote the set of all circuits of $M$.
Let $A$ be a dependent subset.
Then:
:$\exists C \in \mathscr C : C \subseteq A$

Proof:
Consider the ordered set $\struct {\powerset S \setminus \mathscr I, \subseteq}$.
From Element of Finite Ordered Set is Between Maximal and Minimal Elements:
:$\exists C \in \mathscr I : C \subseteq A$ and $A$ is minimal in $\struct {\powerset S \setminus \mathscr I, \subseteq}$.
By definition of a circuit:
:$C \in \mathscr C$
{{qed}}
Category:Matroid Dependent Subsets
Category:Matroid Circuits
ih5crdyz2z7cgbmezkffjm1prsobkig
Theorem: Condition for Linear Operation on Complex Numbers to be of Finite Order

Let $A$ be the operation on the complex numbers $\C$ defined as:
:$\map A x = \alpha x + \beta$
Then $A$ is of finite order greater than $1$ {{iff}} $\alpha$ is a root of unity other than $1$.

Proof:
{{ProofWanted|Not completely sure I understand the context}}
Theorem: Positive Rational Numbers under Division do not form Group

Let $\struct {\Q_{>0}, /}$ denote the algebraic structure consisting of the set of (strictly) positive rational numbers $\Q_{>0}$ under the operation $/$ of division.
We have that $\struct {\Q_{>0}, /}$ is not a group.

Proof:
In order to be a group, it is necessary that $\struct {\Q_{>0}, /}$ be an associative structure.
But consider the elements $2, 6, 12$ of $\Q_{>0}$.
We have:
{{begin-eqn}}
{{eqn | l = \paren {12 / 6} / 2
      | r = 2 / 1
      | c = 
}}
{{eqn | r = 1
      | c = 
}}
{{end-eqn}}
whereas:
{{begin-eqn}}
{{eqn | l = 12 / \paren {6 / 2}
      | r = 12 / 3
      | c = 
}}
{{eqn | r = 4
      | c = 
}}
{{end-eqn}}
That is:
:$\paren {12 / 6} / 2 \ne 12 / \paren {6 / 2}$
So it is not generally the case that for $a, b, c \in \Q_{>0}$:
:$\paren {a / b} / c = a / \paren {b / c}$
and so $/$ is not associative on $\Q_{>0}$.
Hence $\struct {\Q_{>0}, /}$ is not a group.
{{qed}}
Theorem: Derivative of Real Area Hyperbolic Sine of x over a/Corollary 1

:$\map {\dfrac \d {\d x} } {\ln \size {x + \sqrt {x^2 + a^2} } } = \dfrac 1 {\sqrt {x^2 + a^2} }$

Proof:
{{begin-eqn}}
{{eqn | l = \map \arsinh {\frac x a}
      | r = \map \ln {\frac x a + \sqrt {\paren {\frac x a}^2 + a^2} }
      | c = {{Defof|Real Area Hyperbolic Sine}}
}}
{{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 | ll= \leadsto
      | l = \map {\dfrac \d {\d x} } {\map \ln {x + \sqrt {x^2 + a^2} } }
      | r = \map {\dfrac \d {\d x} } {\map \arsinh {\frac x a} + \ln a }
      | c = 
}}
{{eqn | r = \dfrac 1 {\sqrt {x^2 + a^2} } + \map {\dfrac \d {\d x} } {\ln a}
      | c = Derivative of Real Area Hyperbolic Sine of x over a
}}
{{eqn | r = \dfrac 1 {\sqrt {x^2 + a^2} } + 0
      | c = Derivative of Constant
}}
{{end-eqn}}
We have that $\sqrt {x^2 + a^2} > x$ for all $x$.
Thus:
{{begin-eqn}}
{{eqn | l = x + \sqrt {x^2 + a^2}
      | o = >
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \size {x + \sqrt {x^2 + a^2} }
      | r = x + \sqrt {x^2 + a^2}
      | c = {{Defof|Absolute Value}}
}}
{{eqn | ll= \leadsto
      | l = \map {\dfrac \d {\d x} } {\size {x + \sqrt {x^2 + a^2} } }
      | r = \map {\dfrac \d {\d x} } {\map \ln {x + \sqrt {x^2 + a^2} } }
      | c = 
}}
{{end-eqn}}
and the result follows.
{{qed}}
Theorem: Negative of Logarithm of x plus Root x squared plus a squared

Let $x \in \R$ be a real number.
Then:
:$-\map \ln {x + \sqrt {x^2 + a^2} } = \map \ln {-x + \sqrt {x^2 + a^2} } - \map \ln {a^2}$

Proof:
We have that $\sqrt {x^2 + a^2} > x$ for all $x$.
Thus:
:$x + \sqrt {x^2 + a^2} > 0$
and so $\map \ln {x + \sqrt {x^2 + a^2} }$ is defined for all $x$.
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: Derivative of Real Area Hyperbolic Sine of x over a/Corollary 2

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

Proof:
{{begin-eqn}}
{{eqn | l = -\map \arsinh {\frac x a}
      | r = \map \arsinh {-\frac x a}
      | c = Inverse Hyperbolic Sine is Odd Function
}}
{{eqn | r = \map \ln {-\paren {\frac x a} + \sqrt {\paren {-\frac x a}^2 + a^2} }
      | c = {{Defof|Real Area Hyperbolic Sine}}
}}
{{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 = \ln \size {x - \sqrt {x^2 + a^2} } - \ln a
      | c = as $\sqrt {x^2 + a^2} > -x$
}}
{{eqn | ll= \leadsto
      | l = \map {\dfrac \d {\d x} } {\ln \size {x - \sqrt {x^2 + a^2} } }
      | r = \map {\dfrac \d {\d x} } {-\map \arsinh {\frac x a} + \ln a}
      | c = Sum of Logarithms
}}
{{eqn | r = -\dfrac 1 {\sqrt {x^2 + a^2} } + \map {\dfrac \d {\d x} } {\ln a}
      | c = Derivative of Real Area Hyperbolic Sine of x over a
}}
{{eqn | r = -\dfrac 1 {\sqrt {x^2 + a^2} } + 0
      | c = Derivative of Constant
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of Root of x squared plus 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 = \map \ln {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 = -\map \ln {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 = {{Corollary|Negative of Logarithm of x plus Root x squared plus a squared|disp = Negative of Logarithm of $x + \sqrt {x^2 + a^2}$}}
}}
{{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 Cosine of x over a/Corollary 1

:$\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 | ll= \leadsto
      | l = \map {\dfrac \d {\d x} } {\map \ln {x + \sqrt {x^2 - a^2} } }
      | r = \map {\dfrac \d {\d x} } {\map \arcosh {\frac x a} - \ln a }
      | c = 
}}
{{eqn | r = \dfrac 1 {\sqrt {x^2 - a^2} } + \map {\dfrac \d {\d x} } {\ln a}
      | 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}}