avewright/proofwiki-math huggingface dataset:
Theorem: Primitive of Power of Root of x squared minus a squared

:$\ds \int \paren {\sqrt {x^2 - a^2} }^n \rd x = \dfrac {x \paren {\sqrt {x^2 - a^2} }^n} {n + 1} - \dfrac {n a^2} {n + 1} \int \paren {\sqrt {x^2 - a^2} }^{n - 2} \rd x$
for $n \ne -1$

Proof:
Let:
{{begin-eqn}}
{{eqn | l = x
      | r = a \cosh \theta
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = \frac {\d x} {\d \theta}
      | r = a \sinh \theta
      | c = Derivative of Hyperbolic Cosine
}}
{{end-eqn}}
Also:
{{begin-eqn}}
{{eqn | l = x
      | r = a \cosh \theta
}}
{{eqn | ll= \leadsto
      | l = x^2 - a^2
      | r = a^2 \cosh^2 \theta - a^2
      | c = 
}}
{{eqn | r = a^2 \paren {\cosh^2 \theta - 1}
      | c = 
}}
{{eqn | r = a^2 \sinh^2 \theta
      | c = Difference of Squares of Hyperbolic Cosine and Sine
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = \paren {\sqrt {x^2 - a^2} }^n
      | r = a^n \sinh^n \theta
      | c = 
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \int \paren {\sqrt {x^2 - a^2} }^n \rd x
      | r = \int \paren {\sqrt {x^2 - a^2} }^n \, a \sinh \theta \rd \theta
      | c = Integration by Substitution from $(1)$
}}
{{eqn | r = \int a^{n + 1} \sinh^{n + 1} \theta \rd \theta
      | c = substituting for $\paren {\sqrt {x^2 - a^2} }^n$ from $(2)$
}}
{{eqn | r = a^{n + 1} \int \sinh^{n + 1} \theta \rd \theta
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = a^{n + 1} \paren {\frac {\sinh^n \theta \cosh \theta} {n + 1} - \frac n {n + 1} \int \sinh^{n - 1} \theta \rd \theta}
      | c = Primitive of $\sinh^{n + 1} \theta$ for $n \ne -1$
}}
{{eqn | r = \frac {a^n \sinh^n \theta \cdot a \cosh \theta} {n + 1} - a^2 \frac n {n + 1} \int a^{n - 2} \sinh^{n - 2} \theta \cdot a \sinh \theta \rd \theta
      | c = rearranging
}}
{{eqn | r = \frac {x \paren {\sqrt {x^2 - a^2} }^n} {n + 1} - \frac {n a^2} {n + 1} \int \paren {\sqrt {x^2 - a^2} }^{n - 2} \rd x
      | c = substituting for $\sinh \theta$ and $\cosh \theta$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of Power of Root of x squared minus a squared

:$\ds \int \dfrac {\d x} {\paren {\sqrt {x^2 - a^2} }^n} = \dfrac {x \paren {\sqrt {x^2 - a^2} }^{2 - n} } {\paren {2 - n} a^2} - \dfrac {n - 3} {\paren {n - 2} a^2}  \int \dfrac {\d x} {\paren {\sqrt {x^2 - a^2} }^{n - 2} }$
for $n \ne 2$.

Proof:
Let:
{{begin-eqn}}
{{eqn | l = x
      | r = a \cosh \theta
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = \frac {\d x} {\d \theta}
      | r = a \sinh \theta
      | c = Derivative of Hyperbolic Cosine
}}
{{end-eqn}}
Also:
{{begin-eqn}}
{{eqn | l = x
      | r = a \cosh \theta
}}
{{eqn | ll= \leadsto
      | l = x^2 - a^2
      | r = a^2 \cosh^2 \theta - a^2
      | c = 
}}
{{eqn | r = a^2 \paren {\cosh^2 \theta - 1}
      | c = 
}}
{{eqn | r = a^2 \sinh^2 \theta
      | c = Difference of Squares of Hyperbolic Cosine and Sine
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = \paren {\sqrt {x^2 - a^2} }^n
      | r = a^n \sinh^n \theta
      | c = 
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = x
      | r = a \cosh \theta
}}
{{eqn | n = 3
      | ll= \leadsto
      | l = \theta
      | r = \cosh^{-1} \frac x a
      | c = {{Defof|Inverse Hyperbolic Cosine/Real|index = 1|Real Inverse Hyperbolic Cosine}}
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \int \dfrac {\d x} {\paren {\sqrt {x^2 - a^2} }^n}
      | r = \int \dfrac {a \sinh \theta \rd \theta} {\paren {\sqrt {x^2 - a^2} }^n}
      | c = Integration by Substitution from $(1)$
}}
{{eqn | r = \int \dfrac {a \sinh \theta \rd \theta} {a^n \sinh^n \theta}
      | c = substituting for $\paren {\sqrt {x^2 - a^2} }^n$ from $(2)$
}}
{{eqn | r = \dfrac 1 {a^{n - 1} } \int \dfrac {\d \theta} {\sinh^{n - 1} \theta}
      | c = Primitive of Constant Multiple of Function and simplification
}}
{{eqn | r = \dfrac 1 {a^{n - 1} } \paren {\frac {-\cosh \theta} {\paren {n - 2} \sinh^{n - 2} \theta} - \frac {n - 3} {n - 2} \int \frac {\d \theta} {\sinh^{n - 3} \theta} }
      | c = Primitive of $\dfrac 1 {\sinh^{n - 1} \theta}$ for $n \ne 2$
}}
{{eqn | r = \frac {-a \cosh \theta} {\paren {n - 2} a^{n - 2} \sinh^{n - 2} \theta} - \frac {n - 3} {\paren {n - 2} a^2} \int \frac {a \sinh \theta \rd \theta} {a^{n - 2} \sinh^{n - 2} \theta}
      | c = rearranging
}}
{{eqn | r = \frac {-x} {\paren {n - 2} \paren {\sqrt {x^2 - a^2} }^{n - 2} } - \frac {n - 3} {\paren {n - 2} a^2} \int \frac {\d x} {\paren {\sqrt {x^2 - a^2} }^{n - 2} }
      | c = substituting for $\sinh \theta$ and $\cosh \theta$
}}
{{eqn | r = \dfrac {x \paren {\sqrt {x^2 - a^2} }^{2 - n} } {\paren {2 - n} a^2} - \frac {n - 3} {\paren {n - 2} a^2} \int \frac {\d x} {\paren {\sqrt {x^2 - a^2} }^{n - 2} }
      | c = rearranging into given form
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of x by Power of Root of x squared minus a squared

:$\ds \int x \paren {\sqrt {x^2 - a^2} }^n \rd x = \dfrac {\paren {\sqrt {x^2 - a^2} }^{n + 2} } {n + 2} + C$
for $n \ne -2$.

Proof:
Let:
{{begin-eqn}}
{{eqn | l = z
      | r = x^2
}}
{{eqn | ll= \leadsto
      | l = \frac {\d z} {\d x}
      | r = 2 x
      | c = Derivative of Power
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = \frac {\d z} 2
      | r = x \rd x
      | c = 
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \int x \paren {\sqrt {x^2 - a^2} }^n \rd x
      | r = \int \paren {\sqrt {z - a^2} }^n \dfrac {\d z} 2
      | c = Integration by Substitution from $(1)$
}}
{{eqn | r = \dfrac 1 2 \int \paren {\sqrt {z - a^2} }^n \rd z
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \dfrac 1 2 \paren {\frac {2 \paren {\sqrt {z - a^2} }^{n + 2} } {n + 2} } + C
      | c = Primitive of $\paren {\sqrt {z - a^2} }^n$ for $n \ne -2$
}}
{{eqn | r = \dfrac {\paren {\sqrt {x^2 - a^2} }^{n + 2} } {n + 2} + C
      | c = substituting $x^2$ for $z$ and simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Root of x squared minus a squared over x squared/Logarithm Form

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

Proof:
Let:
{{begin-eqn}}
{{eqn | l = z
      | r = x^2
}}
{{eqn | ll= \leadsto
      | l = \frac {\d z} {\d x}
      | r = 2 x
      | c = Power Rule for Derivatives
}}
{{eqn | ll= \leadsto
      | l = \int \frac {\sqrt {x^2 - a^2} } {x^2} \rd x
      | r = \int \frac {\sqrt {z - a^2} \rd z} {2 z \sqrt z}
      | c = Integration by Substitution
}}
{{eqn | r = \frac 1 2 \int \frac {\sqrt {z - a^2} \rd z} {z^{3/2} }
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \frac 1 2 \paren {\frac {-\sqrt {z - a^2} } {\frac 1 2 \sqrt z} + \frac 1 2 \int \frac {\d z} {\sqrt z \sqrt {z - a^2} } } + C
      | c = Primitive of $\dfrac {\sqrt {a x + b} } {x^m}$
}}
{{eqn | r = \frac {-\sqrt {x^2 - a^2} } x + \frac 1 2 \int \frac {2 x \rd x} {x \sqrt {x^2 - a^2} } + C
      | c = substituting for $z$
}}
{{eqn | r = \frac {-\sqrt {x^2 - a^2} } x + \int \frac {\d x} {\sqrt {x^2 - a^2} } + C
      | c = simplifying
}}
{{eqn | r = \frac {-\sqrt {x^2 - a^2} } x + \ln \size {x + \sqrt {x^2 - a^2} } + C
      | c = Primitive of $\dfrac 1 {\sqrt {x^2 - a^2} }$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Root of x squared minus a squared over x squared/Inverse Hyperbolic Cosine Form

:$\ds \int \frac {\sqrt {x^2 - a^2} } {x^2} \rd x = \arcosh \dfrac x a - \frac {\sqrt {x^2 - a^2} } x + C$
for $x^2 \ge a^2$.

Proof:
Let:
{{begin-eqn}}
{{eqn | l = \int \frac {\sqrt {x^2 - a^2} } {x^2} \rd x
      | r = \frac {-\sqrt {x^2 - a^2} } x + \ln \size {x + \sqrt {x^2 - a^2} } + C
      | c = Primitive of $\dfrac 1 {\sqrt {x^2 - a^2} }$
}}
{{eqn | r = \frac {-\sqrt {x^2 - a^2} } x + \map \ln {x + \sqrt {x^2 - a^2} } + C
      | c = as $x + \sqrt {x^2 - a^2} \ge 0$ for $x^2 \ge a^2$
}}
{{eqn | r = \map \ln {x + \sqrt {x^2 - a^2} } - \ln a - \frac {\sqrt {x^2 - a^2} } x + C
      | c = subsuming $\ln a$ into constant of integration and rearranging
}}
{{eqn | r = \arcosh \dfrac x a - \frac {\sqrt {x^2 - a^2} } x + C
      | c = Real Area Hyperbolic Cosine of x over a in Logarithm Form
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power of Root of a squared minus x squared

:$\ds \int \paren {\sqrt {a^2 - x^2} }^n \rd x = \dfrac {x \paren {\sqrt {a^2 - x^2} }^n} {n + 1} - \dfrac {n a^2} {n + 1} \int \paren {\sqrt {a^2 - x^2} }^{n - 2} \rd x$
for $n \ne -1$.

Proof:
Let:
{{begin-eqn}}
{{eqn | l = x
      | r = a \sin \theta
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = \frac {\d x} {\d \theta}
      | r = a \cos \theta
      | c = Derivative of Sine Function
}}
{{end-eqn}}
Also:
{{begin-eqn}}
{{eqn | l = x
      | r = a \sin \theta
}}
{{eqn | ll= \leadsto
      | l = \sqrt {a^2 - x^2}
      | r = \sqrt {a^2 \paren {1 - \sin^2 \theta} }
      | c = 
}}
{{eqn | r = \sqrt {a^2 \cos^2 \theta}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | n = 2
      | r = a \cos \theta
      | c = 
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \int \paren {\sqrt {a^2 - x^2} }^n \rd x
      | r = \int \paren {a \cos \theta}^n \cdot a \cos \theta \rd \theta
      | c = Integration by Substitution from $(1)$ and $(2)$
}}
{{eqn | r = a^{n + 1} \int \cos^{n + 1} \theta \rd \theta
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = a^{n + 1} \paren {\frac {\sin \theta \cos^n \theta} {n + 1} - \frac n {n + 1} \int \cos^{n - 1} \theta \rd \theta}
      | c = Primitive of $\cos^{n + 1} \theta$ for $n \ne -1$
}}
{{eqn | r = \frac {a \sin \theta \cdot a^n \cos^n \theta} {n + 1} - a^2 \frac n {n + 1} \int a^{n - 2} \cos^{n - 2} \theta \cdot a \cos \theta \rd \theta
      | c = rearranging
}}
{{eqn | r = \frac {x \paren {\sqrt {a^2 - x^2} }^n} {n + 1} - \frac {n a^2} {n + 1} \int \paren {\sqrt {a^2 - x^2} }^{n - 2} \rd x
      | c = substituting for $\sinh \theta$ and $\cosh \theta$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power of Root of 2 a x minus x squared

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

Proof:
Let $u := x - a$.
Then:
:$\dfrac {\d u} {\d x} = 1$
and:
:$x = u + a$
Then:
{{begin-eqn}}
{{eqn | l = 2 a x - x^2
      | r = 2 a \paren {u + a} - \paren {u + a}^2
      | c = 
}}
{{eqn | r = 2 a u + 2 a^2 - u^2 - 2 a u - a^2
      | c = 
}}
{{eqn | r = a^2 - u^2
      | c = 
}}
{{end-eqn}}
and we have:
{{begin-eqn}}
{{eqn | l = \int \paren {\sqrt {2 a x - x^2} }^n \rd x
      | r = \int \paren {\sqrt {a^2 - u^2} }^n \rd u
      | c = 
}}
{{eqn | r = \dfrac {u \paren {\sqrt {a^2 - u^2} }^n} {n + 1} - \dfrac {n a^2} {n + 1} \int \paren {\sqrt {a^2 - u^2} }^{n - 2} \rd u
      | c = Primitive of $\paren {\sqrt {a^2 - u^2} }^n$
}}
{{eqn | r = \frac {\paren {x - a} \paren {\sqrt {2 a x - x^2} }^n} {n + 1} + \frac {n a^2} {n + 1} \int \paren {\sqrt {2 a x - x^2} }^{n - 2} \rd x
      | c = substituting for $u$ and simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of Power of Root of 2 a x minus x squared

:$\ds \int \dfrac {\d x} {\paren {\sqrt {2 a x - x^2} }^n} = \frac {\paren {x - a} \paren {\sqrt {2 a x - x^2} }^{2 - n} } {\paren {n - 2} a^2} + \frac {n - 3} {\paren {n - 2} a^2} \int \dfrac {\d x} {\paren {\sqrt {2 a x - x^2} }^{n - 2} }$

Proof:
{{begin-eqn}}
{{eqn | l = \int \dfrac {\d x} {\paren {\sqrt {2 a x - x^2} }^{n - 2} }
      | r = \int \paren {\sqrt {2 a x - x^2} }^{2 - n} \rd x
      | c = 
}}
{{eqn | r = \frac {\paren {x - a} \paren {\sqrt {2 a x - x^2} }^{2 - n} } {\paren {2 - n} + 1} + \frac {\paren {2 - n} a^2} {\paren {2 - n} + 1} \int \paren {\sqrt {2 a x - x^2} }^{\paren {2 - n} - 2} \rd x
      | c = Primitive of $\paren {\sqrt {2 a x - x^2} }^{n - 2}$
}}
{{eqn | r = \frac {\paren {x - a} \paren {\sqrt {2 a x - x^2} }^{2 - n} } {3 - n} + \frac {\paren {2 - n} a^2} {3 - n} \int \dfrac {\d x} {\paren {\sqrt {2 a x - x^2} }^n} \rd x
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \frac {n - 3} {\paren {n - 2} a^2} \int \dfrac {\d x} {\paren {\sqrt {2 a x - x^2} }^{n - 2} }
      | r = \frac {n - 3} {\paren {n - 2} a^2} \frac {\paren {x - a} \paren {\sqrt {2 a x - x^2} }^{2 - n} } {3 - n} + \int \dfrac {\d x} {\paren {\sqrt {2 a x - x^2} }^n} \rd x
      | c = multiplying both sides by $\dfrac {n - 3} {\paren {n - 2} a^2}$
}}
{{eqn | r = -\frac {\paren {x - a} \paren {\sqrt {2 a x - x^2} }^{2 - n} } {\paren {n - 2} a^2} + \int \dfrac {\d x} {\paren {\sqrt {2 a x - x^2} }^n} \rd x
      | c = simplifying
}}
{{end-eqn}}
from which the result follows immediately.
{{qed}}
Theorem: Primitive of x by Root of 2 a x minus x squared

:$\ds \int x \sqrt {2 a x - x^2} \rd x = \frac {\paren {x + a} \paren {2 x - 3 a} \sqrt {2 a x - x^2} } 6 + \frac {a^3} 2 \arcsin \dfrac {x - a} a + C$

Proof:
Let $u := x - a$.
Then:
:$\dfrac {\d u} {\d x} = 1$
and:
:$x = u + a$
Then:
{{begin-eqn}}
{{eqn | l = 2 a x - x^2
      | r = 2 a \paren {u + a} - \paren {u + a}^2
      | c = 
}}
{{eqn | r = 2 a u + 2 a^2 - u^2 - 2 a u - a^2
      | c = 
}}
{{eqn | r = a^2 - u^2
      | c = 
}}
{{end-eqn}}
and we have:
{{begin-eqn}}
{{eqn | l = \int x \sqrt {2 a x - x^2} \rd x
      | r = \int \paren {u + a} \sqrt {a^2 - u^2} \rd u
      | c = 
}}
{{eqn | r = \int u \sqrt {a^2 - u^2} \rd u + a \int \sqrt {a^2 - u^2} \rd u
      | c = Linear Combination of Primitives
}}
{{eqn | r = \frac {-\paren {\sqrt {a^2 - u^2} }^3} 3 - a \int \sqrt {a^2 - u^2} \rd u
      | c = Primitive of $u \sqrt {a^2 - u^2}$
}}
{{eqn | r = \frac {-\paren {a^2 - u^2} \sqrt {a^2 - u^2} } 3 - a \paren {\frac {u \sqrt {a^2 - u^2} } 2 + \frac {a^2} 2 \arcsin \frac u a} + C
      | c = Primitive of $\sqrt {a^2 - u^2}$: Arcsine Form
}}
{{eqn | r = \frac {-\paren {2 a x - x^2} \sqrt {2 a x - x^2} } 3 - \frac {a \paren {x - a} \sqrt {2 a x - x^2} } 2 + \frac {a^3} 2 \arcsin \frac {x - a} a + C
      | c = substituting for $u$ and simplifying
}}
{{end-eqn}}
The result follows after algebra.
{{finish|Well it would do if anyone cares to finish it}}
{{qed}}
Theorem: Primitive of Root of 2 a x minus x squared over x

:$\ds \int \dfrac {\sqrt {2 a x - x^2} } x \rd x = \sqrt {2 a x - x^2} + a \arcsin \dfrac {x - a} a + C$

Proof:
Let $u := x - a$.
Then:
:$\dfrac {\d u} {\d x} = 1$
and:
:$x = u + a$
Then:
{{begin-eqn}}
{{eqn | l = 2 a x - x^2
      | r = 2 a \paren {u + a} - \paren {u + a}^2
      | c = 
}}
{{eqn | r = 2 a u + 2 a^2 - u^2 - 2 a u - a^2
      | c = 
}}
{{eqn | r = a^2 - u^2
      | c = 
}}
{{end-eqn}}
and we have:
{{begin-eqn}}
{{eqn | l = \int \dfrac {\sqrt {2 a x - x^2} } x \rd x
      | r = \int \dfrac {\sqrt {a^2 - u^2} } {u + a} \rd u
      | c = 
}}
{{eqn | r = \int \sqrt {\dfrac {a^2 - u^2} {\paren {a + u}^2} } \rd u
      | c = 
}}
{{eqn | r = \int \sqrt {\dfrac {a - u} {a + u} } \rd u
      | c = Difference of Two Squares and cancelling $a + x$
}}
{{eqn | r = \sqrt {a^2 - u^2} + a \arcsin \dfrac u a + C
      | c = result to be found
}}
{{eqn | r = \sqrt {2 a x - x^2} + a \arcsin \dfrac {x - a} a + C
      | c = substituting for $u$ and simplifying
}}
{{end-eqn}}
{{finish|There's a result in there somewhere.}}
Theorem: Primitive of Root of 2 a x minus x squared over x squared

:$\ds \int \dfrac {\sqrt {2 a x - x^2} } {x^2} \rd x = -2 \sqrt {\dfrac {2 a - x} x} - \arcsin \dfrac {x - a} a + C$

Proof:
With a view to expressing the primitive in the form:
:$\ds \int u \frac {\d v} {\d x} \rd x = u v - \int v \frac {\d u} {\d x} \rd x$
let:
{{begin-eqn}}
{{eqn | l = u
      | r = \sqrt {2 a x - x^2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = \dfrac {2 a - 2 x} {2 \sqrt {2 a x - x^2} }
      | c = Derivative of Power, Chain Rule for Derivatives
}}
{{eqn | r = \dfrac {a - x} {\sqrt {2 a x - x^2} }
      | c = simplifying
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = \dfrac 1 {x^2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = -\dfrac 1 x
      | c = Derivative of Power
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \dfrac {\sqrt {2 a x - x^2} } {x^2} \rd x
      | r = \int u \frac {\d v} {\d x} \rd x
      | c = 
}}
{{eqn | r = \paren {\sqrt {2 a x - x^2} } \paren {-\dfrac 1 x} - \int \paren {-\dfrac 1 x} \paren {\dfrac {a - x} {\sqrt {2 a x - x^2} } } \rd x
      | c = Integration by Parts
}}
{{eqn | r = -\sqrt {\dfrac {x \paren {2 a - x} } {x^2} } + \int \dfrac {a - x} {x \sqrt {2 a x - x^2} } \rd x
      | c = simplifying
}}
{{eqn | r = -\sqrt {\dfrac {2 a - x} x} + a \int \dfrac 1 {x \sqrt {2 a x - x^2} } \rd x - \int \dfrac 1 {\sqrt {2 a x - x^2} } \rd x
      | c = Linear Combination of Primitives
}}
{{eqn | r = -\sqrt {\dfrac {2 a - x} x} + a \paren {-\dfrac 1 a \sqrt {\dfrac {2 a - x} x} } - \int \dfrac 1 {\sqrt {2 a x - x^2} } \rd x
      | c = Primitive of $\dfrac 1 {x \sqrt {2 a x - x^2} }$
}}
{{eqn | r = -\sqrt {\dfrac {2 a - x} x} - \sqrt {\dfrac {2 a - x} x} - \arcsin \dfrac {x - a} a + C
      | c = Primitive of $\dfrac 1 {\sqrt {2 a x - x^2} }$
}}
{{eqn | r = -2 \sqrt {\dfrac {2 a - x} x} - \arcsin \dfrac {x - a} a + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Characterization of Locale

Let $L = \struct{S, \preceq}$ be an ordered set.
{{TFAE}}
:$(1): \quad L$ is a locale
:$(2): \quad L$ is a frame
:$(3): \quad L$ is a complete lattice satisfying the infinite join distributive law
:$(4): \quad L$ is a complete Heyting algebra
:$(5): \quad L$ is a complete Brouwerian lattice

Proof:
=== Statement $(1)$ {{iff}} Statement $(2)$ ===
The equivalence of Statement $(1)$ and Statement $(2)$ follows immediately from the definition of locale
{{qed|lemma}}
Theorem: Primitive of x over Root of 2 a x minus x squared

:$\ds \int \dfrac x {\sqrt {2 a x - x^2} } \rd x = a \arcsin \dfrac {x - a} a - \sqrt {2 a x - x^2} + C$

Proof:
Let $u := x - a$.
Then:
:$\dfrac {\d u} {\d x} = 1$
and:
:$x = u + a$
Then:
{{begin-eqn}}
{{eqn | l = 2 a x - x^2
      | r = 2 a \paren {u + a} - \paren {u + a}^2
      | c = 
}}
{{eqn | r = 2 a u + 2 a^2 - u^2 - 2 a u - a^2
      | c = 
}}
{{eqn | r = a^2 - u^2
      | c = 
}}
{{end-eqn}}
and we have:
{{begin-eqn}}
{{eqn | l = \int \dfrac x {\sqrt {2 a x - x^2} } \rd x
      | r = \int \dfrac {u + a} {\sqrt {a^2 - u^2} } \rd u
      | c = 
}}
{{eqn | r = \int \dfrac u {\sqrt {a^2 - u^2} } \rd u + a \int \dfrac 1 {\sqrt {a^2 - u^2} } \rd u
      | c = Linear Combination of Primitives
}}
{{eqn | r = -\sqrt {a^2 - u^2} + a \paren {\arcsin \frac x a}
      | c = Primitive of $\dfrac u {\sqrt {a^2 - u^2} }$ and Primitive of $\dfrac 1 {\sqrt {a^2 - u^2} }$: Arcsine Form
}}
{{eqn | r = a \arcsin \dfrac {x - a} a - \sqrt {2 a x - x^2} + C
      | c = substituting for $u$ and simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of x by Root of 2 a x minus x squared

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

Proof:
Recall Primitive of $\dfrac 1 {\paren {p x + q} \sqrt {\paren {a x + b} \paren {p x + q} } }$:
{{:Primitive of Reciprocal of p x + q by Root of a x + b by Root of p x + q}}
Then:
{{begin-eqn}}
{{eqn | l = \int \dfrac 1 {x \sqrt {2 a x - x^2} } \rd x
      | r = \int \dfrac 1 {x \sqrt {x \paren {2 a - x} } } \rd x
      | c = manipulating subject into correct form
}}
{{eqn | r = \frac {2 \sqrt {2 a - x} } {\paren {\paren {-1} \times 0 - 2 a \times 1} \sqrt {1 \times x + 0} } + C
      | c = $p \gets 1$, $q \gets 0$, $a \gets -1$, $b \gets 2 a$
}}
{{eqn | r = \frac {2 \sqrt {2 a - x} } {\paren {-2 a} \sqrt x} + C
      | c = simplification
}}
{{eqn | r = -\dfrac 1 a \sqrt {\dfrac {2 a - x} x} + C
      | c = simplification
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Cosine of a x over Sine of a x

:$\ds \int \dfrac {\cos a x} {\sin a x} \rd x = \dfrac 1 a \ln \size {\sin a x} + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \dfrac {\cos a x} {\sin a x} \rd x 
      | r = \int \cot a x \rd x 
      | c = Cotangent is Cosine divided by Sine
}}
{{eqn | r = \dfrac 1 a \ln \size {\sin a x} + C
      | c = Primitive of $\cot a x$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Sine of a x over Cosine of a x

:$\ds \int \dfrac {\sin a x} {\cos a x} \rd x = -\dfrac 1 a \ln \size {\cos a x} + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \dfrac {\sin a x} {\cos a x} \rd x 
      | r = \int \cot a x \rd x 
      | c = Tangent is Sine divided by Cosine
}}
{{eqn | r = -\dfrac 1 a \ln \size {\cos a x} + C
      | c = Primitive of $\tan a x$: Cosine Form
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power of x by Sine of a x/Lemma

:$\ds \int x^m \sin a x \rd x = \frac {- x^m \cos a x} a + \frac m a \int x^{m - 1} \cos a x \rd x$

Proof:
With a view to expressing the primitive in the form:
:$\ds \int u \frac {\d v} {\d x} \rd x = u v - \int v \frac {\d u} {\d x} \rd x$
let:
{{begin-eqn}}
{{eqn | l = u
      | r = x^m
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = m x^{m - 1}
      | c = Power Rule for Derivatives
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = \sin a x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {-\cos a x} a
      | c = Primitive of $\sin a x$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int x^m \sin a x \rd x
      | r = \paren {x^m} \paren {\frac {-\cos a x} a} - \int \paren {\frac {-\cos a x} a} \paren {m x^{m - 1} } \rd x
      | c = Integration by Parts
}}
{{eqn | r = \frac {- x^m \cos a x} a + \frac m a \int x^{m - 1} \cos a x \rd x
      | c = Primitive of Constant Multiple of Function
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power of x by Cosine of a x/Lemma

:$\ds \int x^m \cos a x \rd x = \frac {x^m \sin a x} a - \frac m a \int x^{m - 1} \sin a x \rd x$

Proof:
With a view to expressing the primitive in the form:
:$\ds \int u \frac {\d v} {\d x} \rd x = u v - \int v \frac {\d u} {\d x} \rd x$
let:
{{begin-eqn}}
{{eqn | l = u
      | r = x^m
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = m x^{m - 1}
      | c = Power Rule for Derivatives
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = \cos a x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {\sin a x} a
      | c = Primitive of $\cos a x$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int x^m \cos a x \rd x
      | r = \paren {x^m} \paren {\frac {\sin a x} a} - \int \paren {\frac {\sin a x} a} \paren {m x^{m - 1} } \rd x
      | c = Integration by Parts
}}
{{eqn  | r = \frac {x^m \sin a x} a - \frac m a \int x^{m - 1} \sin a x \rd x
      | c = Primitive of Constant Multiple of Function
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Cosecant of a x/Cosecant plus Cotangent Form

:$\ds \int \csc a x \rd x = -\frac 1 a \ln \size {\csc a x + \cot a x} + C$
where $\csc a x + \cot a x \ne 0$.

Proof:
{{begin-eqn}}
{{eqn | l = \int \csc x \rd x
      | r = -\ln \size {\csc x + \cot x} + C
      | c = Primitive of $\csc x$: Cosecant plus Cotangent Form
}}
{{eqn | ll= \leadsto
      | l = \int \csc a x \rd x
      | r = -\frac 1 a \ln \size {\csc a x + \cot a x} + C
      | c = Primitive of Function of Constant Multiple
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Arcsine of a x

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

Proof:
{{begin-eqn}}
{{eqn | l = \int \arcsin x \rd x
      | r = x \arcsin x + \sqrt {1 - x^2} + C
      | c = Primitive of $\arcsin x$
}}
{{eqn | ll= \leadsto
      | l = \int \arcsin a x \rd x
      | r = \dfrac 1 a \paren {\paren {a x} \arcsin a x + \sqrt {1 - \paren {a x}^2} } + C
      | c = Primitive of Function of Constant Multiple
}}
{{eqn | r = x \arcsin a x + \dfrac 1 a \sqrt {1 - a^2 x^2} + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Arctangent of a x

:$\ds \int \arctan a x \rd x = x \arctan a x - \dfrac 1 {2 a} \map \ln {1 + a^2 x^2} + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \arctan x \rd x
      | r = x \arctan x - \dfrac 1 2 \map \ln {1 + x^2} + C
      | c = Primitive of $\arctan x$
}}
{{eqn | ll= \leadsto
      | l = \int \arctan a x \rd x
      | r = \dfrac 1 a \paren {\paren {a x} \arctan a x - \dfrac 1 2 \map \ln {1 + a^2 x^2} } + C
      | c = Primitive of Function of Constant Multiple
}}
{{eqn | r = x \arctan a x - \dfrac 1 {2 a} \map \ln {1 + a^2 x^2} + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}