avewright/proofwiki-math huggingface dataset:
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 = \tanh^{-1} {\frac x a}
      | c = {{Defof|Real Inverse Hyperbolic Tangent}}, which is defined where $\size {\dfrac x a} < 1$
}}
{{eqn | ll=\leadsto
      | l = x
      | r = a \tanh u
      | c = 
}}
{{eqn | ll=\leadsto
      | l = \frac {\d x} {\d u}
      | r = a \sech^2 u
      | c = Derivative of Hyperbolic Tangent
}}
{{eqn | ll=\leadsto
      | l = \int \frac {\rd x} {a^2 - x^2}
      | r = \int \frac {a \sech^2 u} {a^2 - a^2 \tanh^2 u} \rd u
      | c = Integration by Substitution
}}
{{eqn | r = \frac a {a^2} \int \frac {\sech^2 u} {1 - \tanh^2 u} \rd u
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \frac 1 a \int \frac {\sech^2 u} {\sech^2 u} \rd u
      | c = Sum of Squares of Hyperbolic Secant and Tangent
}}
{{eqn | r = \frac 1 a \int \rd u
}}
{{eqn | r = \frac 1 a u + C
      | c = Integral of Constant
}}
{{eqn | r = \frac 1 a \tanh^{-1} \frac x a + C
      | c = Definition of $u$
}}
{{end-eqn}}
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$.
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

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$.
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

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$.
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

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$.
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 Root of x squared plus a squared/Logarithm Form

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

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {\sqrt {x^2 + a^2} }
      | r = \arsinh {\frac x a} + C
      | c = Primitive of $\dfrac 1 {\sqrt {x^2 + a^2} }$ in $\arsinh$ form
}}
{{eqn | r = \map \ln {x + \sqrt {x^2 + a^2} } - \ln a + C
      | c = $\arsinh \dfrac x a$ in Logarithm Form
}}
{{eqn | r = \map \ln {x + \sqrt {x^2 + a^2} } + C
      | c = subsuming $-\ln a$ into arbitrary constant
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of Root of x squared plus a squared/Logarithm Form

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

Proof:
Let $y^2 = a^2 + x^2$.
Then:
{{begin-eqn}}
{{eqn | l = 2 y \frac {\d y} {\d x}
      | r = 2 x
      | c = Power Rule for Derivatives, Chain Rule for Derivatives
}}
{{eqn | ll= \leadsto
      | l = y \frac {\d y} {\d x}
      | r = x
      | c = simplification
}}
{{eqn | ll= \leadsto
      | l = \frac {\d y} x
      | r = \frac {\d x} y
      | c = 
}}
{{eqn | r = \frac {\d x + \d y} {x + y}
      | c = {{LinkWanted|We don't actually have a result for this}}
}}
{{eqn | ll= \leadsto
      | l = \int \frac {\d x} {\sqrt {x^2 + a^2} }
      | r = \int \frac {\d x} y
      | c = substituting for $y$
}}
{{eqn | r = \frac {\d x + \d y} {x + y}
      | c = from above
}}
{{eqn | r = \ln \size {x + y} + C
      | c = Primitive of Function under its Derivative
}}
{{eqn | r = \ln \size {x + \sqrt {x^2 + a^2} } + C
      | c = substituting back
}}
{{eqn | r = \map \ln {x + \sqrt {x^2 + a^2} } + C
      | c = argument of $\ln$ always positive
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of Root of x squared minus a squared/Logarithm Form

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

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {\sqrt {x^2 - a^2} }
      | r = \cosh^{-1} {\frac x a} + C'
      | c = Primitive of Reciprocal of $\sqrt {x^2 - a^2}$: $\cosh^{-1}$ form
}}
{{eqn | r = \map \ln {\frac x a + \sqrt {\paren {\frac x a}^2 - 1} } + C'
      | c = {{Defof|Real Inverse Hyperbolic Cosine}}
}}
{{eqn | r = \map \ln {\frac x a + \sqrt {\frac {x^2 - a^2} {a^2} } } + C'
      | c = rearrangement
}}
{{eqn | r = \map \ln {\frac {x + \sqrt {x^2 - a^2} } a} + C'
      | c = rearrangement
}}
{{eqn | r = \map \ln {x + \sqrt {x^2 - a^2} } - \ln a + C'
      | c = Difference of Logarithms
}}
{{eqn | r = \map \ln {x + \sqrt {x^2 - a^2} } + C
      | c = putting $C = -\ln a + C'$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of x by Root of x squared minus a squared/Arcsecant Form

:$\ds \int \frac {\d x} {x \sqrt {x^2 - a^2} } = \frac 1 a \arcsec \size {\frac x a} + C$
for $0 < a < \size x$.

Proof:
We have that $\sqrt {x^2 - a^2}$ is defined only when $x^2 > a^2$, that is, either:
:$x > a$
or:
:$x < -a$
where it is assumed that $a > 0$.
Consider the arcsecant substitution:
:$u = \arcsec {\dfrac x a}$
which is defined for all $x$ such that $\size {\dfrac x a} \ge 1$.
That is:
:$\size x \ge a$
and it is seen that $u = \arcsec {\dfrac x a}$ is defined over the whole domain of the integrand.
Hence:
{{begin-eqn}}
{{eqn | l = u
      | r = \arcsec {\frac x a}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = a \sec u
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d x} {\d u}
      | r = a \sec u \tan u
      | c = Derivative of Secant Function
}}
{{end-eqn}}
Let $x > a$.
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {x \sqrt {x^2 - a^2} }
      | r = \int \frac {a \sec u \tan u} {a \sec u \sqrt {a^2 \sec^2 u - a^2} } \rd u
      | c = Integration by Substitution
}}
{{eqn | r = \frac a {a^2} \int \frac {\sec u \tan u} {\sec u \sqrt {\sec^2 u - 1} } \rd u
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \frac 1 a \int \frac {\sec u \tan u} {\sec u \tan u} \rd u
      | c = Difference of Squares of Secant and Tangent
}}
{{eqn | r = \frac 1 a \int 1 \rd u
}}
{{eqn | r = \frac 1 a u + C
      | c = Integral of Constant
}}
{{eqn | r = \frac 1 a \arcsec {\frac x a} + C
      | c = Definition of $u$
}}
{{eqn | r = \frac 1 a \arcsec {\frac {\size x} a} + C
      | c = {{Defof|Absolute Value}}: $\size x = x$ for $x > 0$
}}
{{end-eqn}}
Now suppose $x < -a$.
Let $z = -x$.
Then:
:$\d x = -\d z$
and we then have:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {x \sqrt {x^2 - a^2} }
      | r = \int \frac {-\d z} {\paren {-z} \sqrt {\paren {-z}^2 - a^2} }
      | c = Integration by Substitution
}}
{{eqn | r = \int \frac {\d z} {z \sqrt {z^2 - a^2} }
      | c = simplifying
}}
{{eqn | r = \frac 1 a \arcsec {\frac z a} + C
      | c = from above
}}
{{eqn | r = \frac 1 a \arcsec {\frac {\paren {-x} } a} + C
      | c = substituting back for $x$
}}
{{eqn | r = \frac 1 a \arcsec {\frac {\size x} a} + C
      | c = {{Defof|Absolute Value}}: $\size x = -x$ for $x < 0$
}}
{{end-eqn}}
The result follows.
{{qed}}
Theorem: Primitive of Reciprocal of x by Root of x squared plus a squared/Logarithm Form

For $x \in \R_{\ne 0}$:
:$\ds \int \frac {\d x} {x \sqrt {x^2 + a^2} } = -\frac 1 a \map \ln {\frac a x + \frac {\sqrt {a^2 + x^2} } {\size x} } + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {x \sqrt {x^2 + a^2} }
      | r = -\frac 1 a \arcsch \frac x a + C
      | c = Primitive of Reciprocal of $x \sqrt {x^2 + a^2}$: $\arcsch$ form
}}
{{eqn | r = -\frac 1 a \map \ln {\frac a x + \frac {\sqrt {a^2 + x^2} } {\size x} } + C
      | c = $\arcsch \dfrac x a$ in Logarithm Form
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of x by Root of a squared minus x squared/Logarithm Form

For $a > 0$ and $0 < \size x < a$:
:$\ds \int \frac {\d x} {x \sqrt {a^2 - x^2} } = -\frac 1 a \map \ln {\frac {a + \sqrt {a^2 - x^2} } {\size x} } + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {x \sqrt {a^2 - x^2} }
      | r = -\frac 1 a \sech^{-1} {\frac {\size x} a} + C
      | c = Primitive of Reciprocal of $x \sqrt {a^2 - x^2}$: $\sech^{-1}$ form
}}
{{eqn | r = -\frac 1 a \map \ln {\frac {1 + \sqrt {1 - \paren {\frac {\size x} a}^2} } {\frac {\size x} a} } + C
      | c = {{Defof|Inverse Hyperbolic Secant|subdef = Real|index = 2}}
}}
{{eqn | r = -\frac 1 a \map \ln {\frac {a + a \sqrt {1 - \paren {\frac {\size x} a}^2} } {\size x} } + C
      | c = multiplying top and bottom by $a$
}}
{{eqn | r = -\frac 1 a \map \ln {\frac {a + \sqrt {a^2 - a^2 \paren {\frac {\size x} a}^2} } {\size x} } + C
      | c = moving $a$ within the square root
}}
{{eqn | r = -\frac 1 a \map \ln {\frac {a + \sqrt {a^2 - x^2} } {\size x} } + C
      | c = simplifying, noting $\size x^2 = x^2$
}}
{{end-eqn}}
{{qed}}
Theorem: Generalized Integration by Parts

Let $\map f x, \map g x$ be real functions which are integrable and at least $n$ times differentiable.
Then:
{{begin-eqn}}
{{eqn | l = \int f^{\paren n} g \rd x
      | r = \sum_{j \mathop = 0}^{n - 1} \paren {-1}^j f^{\paren {n - j - 1} } g^{\paren j} + \paren {-1}^n \int f g^{\paren n} \rd x
      | c = 
}}
{{eqn | r = f^{\paren {n - 1} } g - f^{\paren {n - 2} } g' + f^{\paren {n - 3} } g' ' - \cdots + \paren {-1}^n \int f g^{\paren n} \rd x
      | c = 
}}
{{end-eqn}}
where $f^{\paren n}$ denotes the $n$th derivative of $f$.

Proof:
Proof by induction:
For all $n \in \N_{> 0}$, let $\map P n$ be the proposition:
:$\ds \int f^{\paren n} g \rd x = \sum_{j \mathop = 0}^{n - 1} \paren {-1}^j f^{\paren {n - j - 1} } g^\paren j + \paren {-1}^n \int f g^{\paren n} \rd x$
Theorem: Primitive of Function of a x + b

:$\ds \int \map F {a x + b} \rd x = \frac 1 a \int \map F u \rd u$
where $u = a x + b$.

Proof:
{{begin-eqn}}
{{eqn | l = u 
      | r = a x + b
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = a
      | c = {{Corollary|Derivative of Function of Constant Multiple}}
}}
{{eqn | ll= \leadsto
      | l = \int \map F {a x + b} \rd x
      | r = \int \frac {\map F u} a \d u
      | c = Primitive of Composite Function
}}
{{eqn | r = \frac 1 a \int \map F u \rd u
      | c = Primitive of Constant Multiple of Function
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Function of Root of a x + b

:$\ds \int \map F {\sqrt {a x + b} } \rd x = \frac 2 a \int u \map F u \rd u$
where $u = \sqrt {a x + b}$.

Proof:
{{begin-eqn}}
{{eqn | l = u 
      | r = \sqrt {a x + b}
      | c = 
}}
{{eqn | l = u 
      | r = \paren {a x + b}^{1/2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = \frac 1 2 \paren {a x + b}^{-1/2} \map {\frac \d {\d x} } {a x + b}
      | c = Chain Rule for Derivatives, Power Rule for Derivatives
}}
{{eqn | r = \frac 1 {2 u} \map {\frac \d {\d x} } {a x + b}
      | c = substituting for $u$
}}
{{eqn | r = \frac a {2 u}
      | c = {{Corollary|Derivative of Function of Constant Multiple}}
}}
{{eqn | ll= \leadsto
      | l = \int \map F {\sqrt {a x + b} } \rd x
      | r = \int \frac {2 u} a \map F u \rd u
      | c = Primitive of Composite Function
}}
{{eqn | r = \frac 2 a \int u \map F u \rd u
      | c = Primitive of Constant Multiple of Function
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Nth Root

Let $n \in \N_{>0}$.
Let $f: \R \to \R$ be the real function defined as $\map f x = \sqrt [n] x$.
Then:
:$\map {f'} x = \dfrac 1 {n \paren {\sqrt [n] x}^{n - 1} }$
everywhere that $\map f x = \sqrt [n] x$ is defined.

Proof:
{{begin-eqn}}
{{eqn | l = \map f x
      | r = \sqrt [n] x
      | c = 
}}
{{eqn | r = x^{1 / n}
      | c = {{Defof|Root of Number|$n$th Root}}
}}
{{eqn | ll= \leadsto
      | l = \map {f'} x
      | r = \frac 1 n x^{\paren {1 / n} - 1}
      | c = Power Rule for Derivatives
}}
{{eqn | r = \frac 1 n x^{\paren {1 / n} \paren {1 - n} }
      | c = rearrangement
}}
{{eqn | r = \frac 1 {n x^{\paren {1 / n} \paren {n - 1} } }
      | c = Exponent Combination Laws: Negative Power
}}
{{eqn | r = \frac 1 {n \paren {\sqrt [n] x}^{n - 1} }
      | c = {{Defof|Root of Number|$n$th Root}}
}}
{{end-eqn}}
{{qed}}
Category:Derivatives
9w8rn3w3xyhtwxxqhhta3jtt17v6ru5
Theorem: Primitive of Function of Nth Root of a x + b

:$\ds \int \map F {\sqrt [n] {a x + b} } \rd x = \frac n a \int u^{n - 1} \map F u \rd u$
where $u = \sqrt [n] {a x + b}$.

Proof:
{{begin-eqn}}
{{eqn | l = u 
      | r = \sqrt [n] {a x + b}
      | c = 
}}
{{eqn | l = u 
      | r = \paren {a x + b}^{1/n}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = \frac 1 {n \paren {\sqrt [n] {a x + b} }^{n - 1} } \map {\frac \d {\d x} } {a x + b}
      | c = Chain Rule for Derivatives, Derivative of Nth Root
}}
{{eqn | r = \frac 1 {n u^{n - 1} } \map {\frac \d {\d x} } {a x + b}
      | c = substituting for $u$
}}
{{eqn | r = \frac a {n u^{n - 1} }
      | c = Derivative of Function of Constant Multiple: Corollary
}}
{{eqn | ll= \leadsto
      | l = \int \map F {\sqrt [n] {a x + b} } \rd x
      | r = \int \frac {n u^{n - 1} } a \map F u \rd u
      | c = Primitive of Composite Function
}}
{{eqn | r = \frac n a \int u^{n - 1} \map F u \rd u
      | c = Primitive of Constant Multiple of Function
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Function of Root of a squared minus x squared

:$\ds \int \map F {\sqrt {a^2 - x^2} } \rd x = a \int \map F {a \cos u} \cos u \rd u$
where $x = a \sin u$.

Proof:
First note that:
{{begin-eqn}}
{{eqn | l = x 
      | r = a \sin u
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sqrt {a^2 - x^2}
      | r = \sqrt {a^2 - \paren {a \sin u}^2}
      | c =
}}
{{eqn | r = a \sqrt {1 - \sin^2 u}
      | c = taking $a$ outside the square root
}}
{{eqn | n = 1
      | r = a \cos u
      | c = Sum of Squares of Sine and Cosine
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = x 
      | r = a \sin u
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d x} {\d u}
      | r = a \cos u
      | c = Derivative of Sine Function
}}
{{eqn | ll= \leadsto
      | l = \int \map F {\sqrt {a^2 - x^2} } \rd x
      | r = \int a \map F {\sqrt {a^2 - x^2} } \cos u \rd u
      | c = Integration by Substitution
}}
{{eqn | r = \int a \map F {a \cos u} \cos u \rd u
      | c = from $(1)$
}}
{{eqn | r = a \int \map F {a \cos u} \cos u \rd u
      | c = Primitive of Constant Multiple of Function
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Function of Root of a squared plus x squared

:$\ds \int \map F {\sqrt {a^2 + x^2} } \rd x = a \int \map F {a \sec u} \sec^2 u \rd u$
where $x = a \tan u$.

Proof:
First note that:
{{begin-eqn}}
{{eqn | l = x 
      | r = a \tan u
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sqrt {a^2 + x^2}
      | r = \sqrt {a^2 + \paren {a \tan u}^2}
      | c =
}}
{{eqn | r = a \sqrt {1 + \tan^2 u}
      | c = taking $a$ outside the square root
}}
{{eqn | r = a \sqrt {\sec^2 u}
      | c = Difference of Squares of Secant and Tangent
}}
{{eqn | n = 1
      | r = a \sec u
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = x 
      | r = a \tan u
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d x} {\d u}
      | r = a \sec^2 u
      | c = Derivative of Tangent Function
}}
{{eqn | ll= \leadsto
      | l = \int \map F {\sqrt {a^2 + x^2} } \rd x
      | r = \int a \map F {\sqrt {a^2 + x^2} } \sec^2 u \rd u
      | c = Integration by Substitution
}}
{{eqn | r = \int a \map F {a \sec u} \sec^2 u \rd u
      | c = from $(1)$
}}
{{eqn | r = a \int \map F {a \sec u} \sec^2 u \rd u
      | c = Primitive of Constant Multiple of Function
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Function of Root of x squared minus a squared

:$\ds \int \map F {\sqrt {x^2 - a^2} } \rd x = a \int \map F {a \tan u} \sec u \tan u \rd u$
where $x = a \sec u$.

Proof:
First note that:
{{begin-eqn}}
{{eqn | l = x 
      | r = a \sec u
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sqrt {x^2 - a^2}
      | r = \sqrt {\paren {a \sec u}^2 - a^2}
      | c =
}}
{{eqn | r = a \sqrt {\sec^2 u - 1}
      | c = taking $a$ outside the square root
}}
{{eqn | r = a \sqrt {\tan^2 u}
      | c = Difference of Squares of Secant and Tangent
}}
{{eqn | n = 1
      | r = a \tan u
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = x 
      | r = a \sec u
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d x} {\d u}
      | r = a \sec u \tan u
      | c = Derivative of Secant Function
}}
{{eqn | ll= \leadsto
      | l = \int \map F {\sqrt {x^2 - a^2} } \rd x
      | r = \int a \map F {\sqrt {x^2 - a^2} } \sec u \tan u \rd u
      | c = Integration by Substitution
}}
{{eqn | r = \int a \map F {a \tan u} \sec u \tan u \rd u
      | c = from $(1)$
}}
{{eqn | r = a \int \map F {a \tan u} \sec u \tan u \rd u
      | c = Primitive of Constant Multiple of Function
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Function of Exponential Function

:$\ds \int \map F {e^{a x} } \rd x = \frac 1 a \int \frac {\map F u} u \rd u$
where $u = e^{a x}$.

Proof:
{{begin-eqn}}
{{eqn | l = u 
      | r = e^{a x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = a e^{a x}
      | c = Derivative of Exponential of a x
}}
{{eqn | r = a u
      | c = Definition of $u$
}}
{{eqn | ll= \leadsto
      | l = \int \map F {e^{a x} } \rd x
      | r = \int \frac {\map F u} {a u} \rd u
      | c = Primitive of Composite Function
}}
{{eqn | r = \frac 1 a \int \frac {\map F u} u \rd u
      | c = Primitive of Constant Multiple of Function
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Function of Natural Logarithm

:$\ds \int \map F {\ln x} \rd x = \int \map F u e^u \rd u$
where $u = \ln x$.

Proof:
{{begin-eqn}}
{{eqn | l = u 
      | r = \ln x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = \frac 1 x
      | c = Derivative of Natural Logarithm Function
}}
{{eqn | ll= \leadsto
      | l = \int \map F {\ln x} \rd x
      | r = \int \map F u x \rd u
      | c = Primitive of Composite Function
}}
{{eqn | r = \int \map F u e^u \rd u
      | c = {{Defof|Exponential Function/Real|subdef = Power Series Expansion|Exponential Function}}
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Function of Arcsine

:$\ds \int \map F {\arcsin \frac x a} \rd x = a \int \map F u \cos u \rd u$
where $u = \arcsin \dfrac x a$.

Proof:
First note that:
{{begin-eqn}}
{{eqn | l = u
      | r = \arcsin \frac x a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = a \sin u
      | c = {{Defof|Real Arcsine}}
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = u 
      | r = \arcsin \frac x a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = \frac 1 {\sqrt {a^2 - x^2} }
      | c = Derivative of Arcsine Function: Corollary
}}
{{eqn | ll= \leadsto
      | l = \int \map F {\arcsin \frac x a} \rd x
      | r = \int \map F u \sqrt {a^2 - x^2} \rd u
      | c = Primitive of Composite Function
}}
{{eqn | r = \int \map F u \sqrt {a^2 - a^2 \sin^2 u} \rd u
      | c = Definition of $x$
}}
{{eqn | r = \int \map F u a \sqrt {1 - \sin^2 u} \rd u
      | c = 
}}
{{eqn | r = \int \map F u a \cos u \rd u
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = a \int \map F u \cos u \rd u
      | c = Primitive of Constant Multiple of Function
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Function of Arccosine

:$\ds \int \map F {\arccos \frac x a} \rd x = -a \int \map F u \sin u \rd u$
where $u = \arccos \dfrac x a$.

Proof:
First note that:
{{begin-eqn}}
{{eqn | l = u
      | r = \arccos \frac x a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = a \cos u
      | c = {{Defof|Real Arccosine}}
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = u 
      | r = \arccos \frac x a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = \frac {-1} {\sqrt {a^2 - x^2} }
      | c = Derivative of Arccosine Function: Corollary
}}
{{eqn | ll= \leadsto
      | l = \int \map F {\arccos \frac x a} \rd x
      | r = \int \map F u \paren {-\sqrt {a^2 - x^2} } \rd u
      | c = Primitive of Composite Function
}}
{{eqn | r = \int \map F u \paren {-\sqrt {a^2 - a^2 \cos^2 u} } \rd u
      | c = Definition of $x$
}}
{{eqn | r = \int \map F u a \paren {-\sqrt {1 - \cos^2 u} } \rd u
      | c = 
}}
{{eqn | r = \int \map F u a \paren {-\sin u} \rd u
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = -a \int\map F u \sin u \rd u
      | c = Primitive of Constant Multiple of Function
}}
{{end-eqn}}
{{qed}}