avewright/proofwiki-math huggingface dataset:
Theorem: Primitive of Composite Function

Let $f$ and $g$ be a real functions which are integrable.
Let the composite function $g \circ f$ also be integrable.
Then:
{{begin-eqn}}
{{eqn | l = \int \map {\paren {g \circ f} } x \rd x
      | r = \int \map g u \frac {\d x} {\d u} \rd u
      | c = 
}}
{{eqn | r = \int \frac {\map g u} {\map {f'} x} \rd u
      | c = 
}}
{{end-eqn}}
where $u = \map f x$.

Proof:
{{begin-eqn}}
{{eqn | l = \map F x
      | r = \int \map {\paren {g \circ f} } x \rd x
}}
{{eqn | r = \int \map g {\map f x} \rd x
      | c = {{Defof|Composition of Mappings}}
}}
{{eqn | r = \int \map g u \rd x
      | c = where $u = \map f x$
}}
{{eqn | ll= \leadsto
      | l = \frac {\d F} {\d x}
      | r = \map g u
      | c = {{Defof|Primitive (Calculus)}}
}}
{{eqn | ll= \leadsto
      | l = \frac {\d F} {\d u} \frac {\d u} {\d x}
      | r = \map g u
      | c = Chain Rule for Derivatives
}}
{{eqn | ll= \leadsto
      | l = \frac {\d F} {\d u} \frac \d {\d x} \map f x
      | r = \map g u
      | c = Definition of $u$
}}
{{eqn | ll= \leadsto
      | l = \frac {\d F} {\d u} \map {f'} x
      | r = \map g u
      | c = {{Defof|Derivative}}
}}
{{eqn | ll= \leadsto
      | l = \frac {\d F} {\d u}
      | r = \frac {\map g u} {\map {f'} x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = F
      | r = \int \frac {\map g u} {\map {f'} x} \rd u
      | c = {{Defof|Primitive (Calculus)}}
}}
{{eqn | r = \int \map g u \frac {\d x} {\d u} \rd u
      | c = Derivative of Inverse Function: $\dfrac {\d x} {\d u} = \dfrac 1 {\d u / \d x}$
}}
{{end-eqn}}
{{qed}}
Theorem: Weierstrass Product Inequality

For $n \ge 1$:
:$\ds \prod_{i \mathop = 1}^n \paren {1 - a_i} \ge 1 - \sum_{i \mathop = 1}^n a_i$
where all of $a_i$ are in the closed interval $\closedint 0 1$.

Proof:
For $n = 1$ we have:
:$1 - a_1 \ge 1 - a_1$
which is clearly true. 
Suppose the proposition is true for $n = k$, that is:
:$\ds \prod_{i \mathop = 1}^k \paren {1 - a_i} \ge 1 - \sum_{i \mathop = 1}^k a_i$
Then:
{{begin-eqn}}
{{eqn | l = \prod_{i \mathop = 1}^{k + 1} \paren {1 - a_i} 
      | r = \paren {1 - a_{k + 1} } \prod_{i \mathop = 1}^k \paren {1 - a_i}
      | c = 
}}
{{eqn | o = \ge
      | r = \paren {1 - a_{k + 1} } \paren {1 - \sum_{i \mathop = 1}^k a_i}
      | c = as $1 - a_{k + 1} \ge 0$
}}
{{eqn | r = 1 - a_{k + 1} - \sum_{i \mathop = 1}^k a_i + a_{k + 1} \sum_{i \mathop = 1}^k a_i
      | c = 
}}
{{eqn | o = \ge
      | r = 1 - a_{k + 1} - \sum_{i \mathop = 1}^k a_i
      | c = as $a_i \ge 0$
}}
{{eqn | r = 1 - \sum_{i \mathop = 1}^{k + 1} a_i
      | c = 
}}
{{end-eqn}}
Thus, by Principle of Mathematical Induction, the proof is complete. 
{{qed}}
Theorem: Primitive of Power

Let $n \in \R: n \ne -1$.
Then:
:$\ds \int x^n \rd x = \frac {x^{n + 1} } {n + 1} + C$
where $C$ is an arbitrary constant.

Proof:
Let $u = \sqrt {a x + b}$.
Then:
{{begin-eqn}}
{{eqn | l = \int \paren {\sqrt {a x + b} }^m \rd x
      | r = \frac 2 a \int u \cdot u^m \rd x
      | c = Primitive of Function of $\sqrt {a x + b}$
}}
{{eqn | r = \frac 2 a \int u^{m + 1} \rd x
      | c = simplifying
}}
{{eqn | r = \frac 2 a \frac {u^{m + 2} } {m + 2} + C
      | c = Primitive of Power valid for $m + 2 \ne 0$, that is, $m \ne -2$
}}
{{eqn | r = \frac {2 \paren {\sqrt {a x + b} }^{m + 2} } {a \paren {m + 2} } + C
      | c = substituting for $u$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power

Let $n \in \R: n \ne -1$.
Then:
:$\ds \int x^n \rd x = \frac {x^{n + 1} } {n + 1} + C$
where $C$ is an arbitrary constant.

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

Let $n \in \R: n \ne -1$.
Then:
:$\ds \int x^n \rd x = \frac {x^{n + 1} } {n + 1} + C$
where $C$ is an arbitrary constant.

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 Power

Let $n \in \R: n \ne -1$.
Then:
:$\ds \int x^n \rd x = \frac {x^{n + 1} } {n + 1} + C$
where $C$ is an arbitrary constant.

Proof:
{{begin-eqn}}
{{eqn | l = \map {\dfrac \d {\d x} } {\frac {\paren {a x + b}^{n + 1} } {\paren {n + 1} a} }
      | r = \dfrac {\paren {n + 1} \paren {a x + b}^n} {\paren {n + 1} a} \map {\dfrac \d {\d x} } {a x + b}
      | c = Power Rule for Derivatives, Chain Rule for Derivatives
}}
{{eqn | r = \dfrac {a \paren {n + 1} \paren {a x + b}^n} {\paren {n + 1} a}
      | c = Power Rule for Derivatives
}}
{{eqn | r = \paren {a x + b}^n
      | c = simplifying
}}
{{end-eqn}}
The result follows by definition of primitive.
{{qed}}
Theorem: Primitive of Power

Let $n \in \R: n \ne -1$.
Then:
:$\ds \int x^n \rd x = \frac {x^{n + 1} } {n + 1} + C$
where $C$ is an arbitrary constant.

Proof:
Recall:
{{begin-eqn}}
{{eqn | n = 1
      | l = \int x^m \arccsc x \rd x
      | r = <nowiki>\begin {cases}
\ds \dfrac {x^{m + 1} } {m + 1} \arccsc x + \dfrac 1 {m + 1} \int \dfrac {x^m \rd x} {\sqrt {x^2 - 1} } & : 0 < \arccsc x < \dfrac \pi 2 \\ \\
\ds \dfrac {x^{m + 1} } {m + 1} \arccsc x - \dfrac 1 {m + 1} \int \dfrac {x^m \rd x} {\sqrt {x^2 - 1} } & : -\dfrac \pi 2 < \arccsc x < 0 \\
\end {cases} </nowiki>
      | c = Primitive of $x^m \arccsc x$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int x^m \arccsc \frac x a \rd x
      | r = \int a^m \paren {\dfrac x a}^m \arccsc \frac x a \rd x
      | c = manipulating into appropriate form
}}
{{eqn | r = a^m \int \paren {\dfrac x a}^m \arccsc \frac x a \rd x
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = <nowiki> a^m \paren {\dfrac 1 {1 / a} \paren {\begin {cases}
\dfrac 1 {m + 1} \paren {\dfrac x a}^{m + 1} \arccsc \dfrac x a + \dfrac 1 {m + 1} \ds \int \paren {\dfrac x a}^m \frac {\d x} {\sqrt {\paren {\dfrac x a}^2 - 1} } & : 0 < \arccsc \dfrac x a < \dfrac \pi 2 \\ \\
\dfrac 1 {m + 1} \paren {\dfrac x a}^{m + 1} \arccsc \dfrac x a - \dfrac 1 {m + 1} \ds \int \paren {\dfrac x a}^m \frac {\d x} {\sqrt {\paren {\dfrac x a}^2 - 1} } & : -\dfrac \pi 2 < \arccsc \dfrac x a < 0
\end {cases} } } </nowiki>
      | c = Primitive of Function of Constant Multiple, from $(1)$
}}
{{eqn | r = <nowiki> \begin {cases}
\dfrac {x^{m + 1} } {m + 1} \arccsc \dfrac x a + \dfrac a {m + 1} \ds \int \dfrac {x^m \rd x} {\sqrt {x^2 - a^2} } & : 0 < \arccsc \dfrac x a < \dfrac \pi 2 \\ \\
\dfrac {x^{m + 1} } {m + 1} \arccsc \dfrac x a - \dfrac a {m + 1} \ds \int \dfrac {x^m \rd x} {\sqrt {x^2 - a^2} } & : -\dfrac \pi 2 < \arccsc \dfrac x a < 0
\end {cases} </nowiki>
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power

Let $n \in \R: n \ne -1$.
Then:
:$\ds \int x^n \rd x = \frac {x^{n + 1} } {n + 1} + C$
where $C$ is an arbitrary constant.

Proof:
With a view to expressing the primitive in the form:
:$\ds \int u \frac {\rd v} {\d x} \rd x = u v - \int v \frac {\d u} {\d x} \rd x$
let:
{{begin-eqn}}
{{eqn | l = u
      | r = \arccsc \frac x a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = <nowiki> \begin {cases} \dfrac {-a} {x \sqrt {x^2 - a^2} } & : 0 < \arccsc \dfrac x a < \dfrac \pi 2 \\
\dfrac a {x \sqrt {x^2 - a^2} } & : -\dfrac \pi 2 < \arccsc \dfrac x a < 0 \\
\end{cases} </nowiki>
      | c = Derivative of $\arccsc \dfrac x a$
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = x^m
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {x^{m + 1} } {m + 1}
      | c = Primitive of Power
}}
{{end-eqn}}
First let $\arccsc \dfrac x a$ be in the interval $\openint 0 {\dfrac \pi 2}$.
Then:
{{begin-eqn}}
{{eqn | l = \int x^m \arccsc \frac x a \rd x
      | r = \frac {x^{m + 1} } {m + 1} \arccsc \frac x a - \int \frac {x^{m + 1} } {m + 1} \paren {\frac {-a} {x \sqrt {x^2 - a^2} } } \rd x
      | c = Integration by Parts
}}
{{eqn | r = \frac {x^{m + 1} } {m + 1} \arccsc \frac x a + \frac a {m + 1} \int \frac {x^m \rd x} {\sqrt {x^2 - a^2} }
      | c = Primitive of Constant Multiple of Function
}}
{{end-eqn}}
Similarly, let $\arccsc \dfrac x a$ be in the interval $\openint {-\dfrac \pi 2}  0$.
Then:
{{begin-eqn}}
{{eqn | l = \int x^m \arccsc \frac x a \rd x
      | r = \frac {x^{m + 1} } {m + 1} \arccsc \frac x a - \int \frac {x^{m + 1} } {m + 1} \paren {\frac a {x \sqrt {x^2 - a^2} } } \rd x
      | c = Integration by Parts
}}
{{eqn | r = \frac {x^{m + 1} } {m + 1} \arccsc \frac x a - \frac a {m + 1} \int \frac {x^m \rd x} {\sqrt {x^2 - a^2} }
      | c = Primitive of Constant Multiple of Function
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power

Let $n \in \R: n \ne -1$.
Then:
:$\ds \int x^n \rd x = \frac {x^{n + 1} } {n + 1} + C$
where $C$ is an arbitrary constant.

Proof:
Recall:
{{begin-eqn}}
{{eqn | n = 1
      | l = \int x^m \arccos x \rd x
      | r = \frac {x^{m + 1} } {m + 1} \arccos x + \frac 1 {m + 1} \int \frac {x^{m + 1} \rd x} {\sqrt {1 - x^2} }
      | c = Primitive of $x^m \arccos x$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int x^m \arccos \frac x a \rd x
      | r = \int a^m \paren {\dfrac x a}^m \arccos \frac x a \rd x
      | c = manipulating into appropriate form
}}
{{eqn | r = a^m \int \paren {\dfrac x a}^m \arccos \frac x a \rd x
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = a^m \paren {\dfrac 1 {1 / a} \paren {\frac 1 {m + 1} \paren {\dfrac x a}^{m + 1} \arccos \frac x a + \frac 1 {m + 1} \int \paren {\dfrac x a}^{m + 1} \frac {\d x} {\sqrt {1 - \paren {\dfrac x a}^2} } } }
      | c = Primitive of Function of Constant Multiple, from $(1)$
}}
{{eqn | r = \frac {x^{m + 1} } {m + 1} \arccos \frac x a + \frac 1 {m + 1} \int \frac {x^{m + 1} \rd x} {\sqrt {a^2 - x^2} } 
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power

Let $n \in \R: n \ne -1$.
Then:
:$\ds \int x^n \rd x = \frac {x^{n + 1} } {n + 1} + C$
where $C$ is an arbitrary constant.

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 = \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 $\arccos \dfrac x a$
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = x^m
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {x^{m + 1} } {m + 1}
      | c = Primitive of Power
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int x^m \arccos \frac x a \rd x
      | r = \frac {x^{m + 1} } {m + 1} \arccos \frac x a - \int \frac {x^{m + 1} } {m + 1} \paren {\frac {-1} {\sqrt {a^2 - x^2} } } \rd x
      | c = Integration by Parts
}}
{{eqn | r = \frac {x^{m + 1} } {m + 1} \arccos \frac x a + \frac 1 {m + 1} \int \frac {x^{m + 1} \rd x} {\sqrt {a^2 - x^2} }
      | c = Primitive of Constant Multiple of Function
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power

Let $n \in \R: n \ne -1$.
Then:
:$\ds \int x^n \rd x = \frac {x^{n + 1} } {n + 1} + C$
where $C$ is an arbitrary constant.

Proof:
Recall:
{{begin-eqn}}
{{eqn | n = 1
      | l = \int x^m \arccot x \rd x
      | r = \frac {x^{m + 1} } {m + 1} \arccot x + \frac 1 {m + 1} \int \frac {x^{m + 1} \rd x} {x^2 + 1}
      | c = Primitive of $x^m \arccot x$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int x^m \arccot \frac x a \rd x
      | r = \int a^m \paren {\dfrac x a}^m \arccot \frac x a \rd x
      | c = manipulating into appropriate form
}}
{{eqn | r = a^m \int \paren {\dfrac x a}^m \arccot \frac x a \rd x
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = a^m \paren {\dfrac 1 {1 / a} \paren {\frac 1 {m + 1} \paren {\dfrac x a}^{m + 1} \arccot \frac x a + \frac 1 {m + 1} \int \paren {\dfrac x a}^{m + 1} \frac {\d x} {\paren {\dfrac x a}^2 + 1} } }
      | c = Primitive of Function of Constant Multiple, from $(1)$
}}
{{eqn | r = \frac {x^{m + 1} } {m + 1} \arccot \frac x a + \frac a {m + 1} \int \frac {x^{m + 1} \rd x} {x^2 + a^2}
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power

Let $n \in \R: n \ne -1$.
Then:
:$\ds \int x^n \rd x = \frac {x^{n + 1} } {n + 1} + C$
where $C$ is an arbitrary constant.

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 = \arccot \frac x a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = \frac {-a} {x^2 + a^2}
      | c = Derivative of $\arccot \dfrac x a$
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = x^m
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {x^{m + 1} } {m + 1}
      | c = Primitive of Power
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int x^m \arccot \frac x a \rd x
      | r = \frac {x^{m + 1} } {m + 1} \arccot \frac x a - \int \frac {x^{m + 1} } {m + 1} \paren {\frac {-a} {x^2 + a^2} } \rd x
      | c = Integration by Parts
}}
{{eqn | r = \frac {x^{m + 1} } {m + 1} \arccot \frac x a + \frac a {m + 1} \int \frac {x^{m + 1} \rd x} {x^2 + a^2}
      | c = Primitive of Constant Multiple of Function
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power

Let $n \in \R: n \ne -1$.
Then:
:$\ds \int x^n \rd x = \frac {x^{n + 1} } {n + 1} + C$
where $C$ is an arbitrary constant.

Proof:
Recall:
{{begin-eqn}}
{{eqn | n = 1
      | l = \int x^m \arcsec x \rd x
      | r = <nowiki>\begin {cases}
\dfrac {x^{m + 1} } {m + 1} \arcsec x - \dfrac 1 {m + 1} \ds \int \dfrac {x^m \rd x} {\sqrt {x^2 - 1} } & : 0 < \arcsec x < \dfrac \pi 2 \\
\dfrac {x^{m + 1} } {m + 1} \arcsec x + \dfrac 1 {m + 1} \ds \int \dfrac {x^m \rd x} {\sqrt {x^2 - 1} } & : \dfrac \pi 2 < \arcsec x < \pi \\
\end {cases} </nowiki>
      | c = Primitive of $x^m \arcsec x$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int x^m \arcsec \frac x a \rd x
      | r = \int a^m \paren {\dfrac x a}^m \arcsec \frac x a \rd x
      | c = manipulating into appropriate form
}}
{{eqn | r = a^m \int \paren {\dfrac x a}^m \arcsec \frac x a \rd x
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = <nowiki> a^m \paren {\dfrac 1 {1 / a} \paren {\begin {cases}
\dfrac 1 {m + 1} \paren {\dfrac x a}^{m + 1} \arcsec \dfrac x a - \dfrac 1 {m + 1} \ds \int \paren {\dfrac x a}^m \frac {\d x} {\sqrt {\paren {\dfrac x a}^2 - 1} } & : 0 < \arcsec \dfrac x a < \dfrac \pi 2 \\
\dfrac 1 {m + 1} \paren {\dfrac x a}^{m + 1} \arcsec \dfrac x a + \dfrac 1 {m + 1} \ds \int \paren {\dfrac x a}^m \frac {\d x} {\sqrt {\paren {\dfrac x a}^2 - 1} } & : \dfrac \pi 2 < \arcsec \dfrac x a < \pi \\
\end {cases} } } </nowiki>
      | c = Primitive of Function of Constant Multiple, from $(1)$
}}
{{eqn | r = <nowiki> \begin {cases}
\dfrac {x^{m + 1} } {m + 1} \arcsec \dfrac x a - \dfrac a {m + 1} \ds \int \dfrac {x^m \rd x} {\sqrt {x^2 - a^2} } & : 0 < \arcsec \dfrac x a < \dfrac \pi 2 \\
\dfrac {x^{m + 1} } {m + 1} \arcsec \dfrac x a + \dfrac a {m + 1} \ds \int \dfrac {x^m \rd x} {\sqrt {x^2 - a^2} } & : \dfrac \pi 2 < \arcsec \dfrac x a < \pi \\
\end {cases} </nowiki>
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power

Let $n \in \R: n \ne -1$.
Then:
:$\ds \int x^n \rd x = \frac {x^{n + 1} } {n + 1} + C$
where $C$ is an arbitrary constant.

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 = \arcsec \frac x a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = <nowiki> \begin {cases} \dfrac a {x \sqrt {x^2 - a^2} } & : 0 < \arcsec \dfrac x a < \dfrac \pi 2 \\
\dfrac {-a} {x \sqrt {x^2 - a^2} } & : \dfrac \pi 2 < \arcsec \dfrac x a < \pi \\
\end {cases} </nowiki>
      | c = Derivative of $\arcsec \dfrac x a$
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = x^m
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {x^{m + 1} } {m + 1}
      | c = Primitive of Power
}}
{{end-eqn}}
First let $\arcsec \dfrac x a$ be in the interval $\openint 0 {\dfrac \pi 2}$.
Then:
{{begin-eqn}}
{{eqn | l = \int x^m \arcsec \frac x a \rd x
      | r = \frac {x^{m + 1} } {m + 1} \arcsec \frac x a - \int \frac {x^{m + 1} } {m + 1} \paren {\frac a {x \sqrt {x^2 - a^2} } } \rd x
      | c = Integration by Parts
}}
{{eqn | r = \frac {x^{m + 1} } {m + 1} \arcsec \frac x a - \frac a {m + 1} \int \frac {x^m \rd x} {\sqrt {x^2 - a^2} }
      | c = Primitive of Constant Multiple of Function
}}
{{end-eqn}}
Similarly, let $\arcsec \dfrac x a$ be in the interval $\openint {\dfrac \pi 2} \pi$.
Then:
{{begin-eqn}}
{{eqn | l = \int x^m \arcsec \frac x a \rd x
      | r = \frac {x^{m + 1} } {m + 1} \arcsec \frac x a - \int \frac {x^{m + 1} } {m + 1} \paren {\frac {-a} {x \sqrt {x^2 - a^2} } } \rd x
      | c = Integration by Parts
}}
{{eqn | r = \frac {x^{m + 1} } {m + 1} \arcsec \frac x a + \frac a {m + 1} \int \frac {x^m \rd x} {\sqrt {x^2 - a^2} }
      | c = Primitive of Constant Multiple of Function
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power

Let $n \in \R: n \ne -1$.
Then:
:$\ds \int x^n \rd x = \frac {x^{n + 1} } {n + 1} + C$
where $C$ is an arbitrary constant.

Proof:
Recall:
{{begin-eqn}}
{{eqn | n = 1
      | l = \int x^m \arcsin x \rd x
      | r = \frac {x^{m + 1} } {m + 1} \arcsin x - \frac 1 {m + 1} \int \frac {x^{m + 1} \rd x} {\sqrt {1 - x^2} }
      | c = Primitive of $x^m \arcsin x$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int x^m \arcsin \frac x a \rd x
      | r = \int a^m \paren {\dfrac x a}^m \arcsin \frac x a \rd x
      | c = manipulating into appropriate form
}}
{{eqn | r = a^m \int \paren {\dfrac x a}^m \arcsin \frac x a \rd x
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = a^m \paren {\dfrac 1 {1 / a} \paren {\frac 1 {m + 1} \paren {\dfrac x a}^{m + 1} \arcsin \frac x a - \frac 1 {m + 1} \int \paren {\dfrac x a}^{m + 1} \frac {\d x} {\sqrt {1 - \paren {\dfrac x a}^2} } } }
      | c = Primitive of Function of Constant Multiple, from $(1)$
}}
{{eqn | r = \frac {x^{m + 1} } {m + 1} \arcsin \frac x a - \frac 1 {m + 1} \int \frac {x^{m + 1} \rd x} {\sqrt {a^2 - x^2} } 
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power

Let $n \in \R: n \ne -1$.
Then:
:$\ds \int x^n \rd x = \frac {x^{n + 1} } {n + 1} + C$
where $C$ is an arbitrary constant.

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 = \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 $\arcsin \dfrac x a$
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = x^m
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {x^{m + 1} } {m + 1}
      | c = Primitive of Power
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int x^m \arcsin \frac x a \rd x
      | r = \frac {x^{m + 1} } {m + 1} \arcsin \frac x a - \int \frac {x^{m + 1} } {m + 1} \paren {\frac 1 {\sqrt {a^2 - x^2} } } \rd x
      | c = Integration by Parts
}}
{{eqn | r = \frac {x^{m + 1} } {m + 1} \arcsin \frac x a - \frac 1 {m + 1} \int \frac {x^{m + 1} \rd x} {\sqrt {a^2 - x^2} }
      | c = Primitive of Constant Multiple of Function
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power

Let $n \in \R: n \ne -1$.
Then:
:$\ds \int x^n \rd x = \frac {x^{n + 1} } {n + 1} + C$
where $C$ is an arbitrary constant.

Proof:
Recall:
{{begin-eqn}}
{{eqn | n = 1
      | l = \int x^m \arctan x \rd x
      | r = \frac {x^{m + 1} } {m + 1} \arctan x - \frac 1 {m + 1} \int \frac {x^{m + 1} \rd x} {x^2 + 1}
      | c = Primitive of $x^m \arctan x$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int x^m \arctan \frac x a \rd x
      | r = \int a^m \paren {\dfrac x a}^m \arctan \frac x a \rd x
      | c = manipulating into appropriate form
}}
{{eqn | r = a^m \int \paren {\dfrac x a}^m \arctan \frac x a \rd x
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = a^m \paren {\dfrac 1 {1 / a} \paren {\frac 1 {m + 1} \paren {\dfrac x a}^{m + 1} \arctan \frac x a - \frac 1 {m + 1} \int \paren {\dfrac x a}^{m + 1} \frac {\d x} {\paren {\dfrac x a}^2 + 1} } }
      | c = Primitive of Function of Constant Multiple, from $(1)$
}}
{{eqn | r = \frac {x^{m + 1} } {m + 1} \arctan \frac x a - \frac a {m + 1} \int \frac {x^{m + 1} \rd x} {x^2 + a^2}
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power

Let $n \in \R: n \ne -1$.
Then:
:$\ds \int x^n \rd x = \frac {x^{n + 1} } {n + 1} + C$
where $C$ is an arbitrary constant.

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 = \arctan \frac x a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = \frac a {x^2 + a^2}
      | c = Derivative of $\arctan \dfrac x a$
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = x^m
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {x^{m + 1} } {m + 1}
      | c = Primitive of Power
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int x^m \arctan \frac x a \rd x
      | r = \frac {x^{m + 1} } {m + 1} \arctan \frac x a - \int \frac {x^{m + 1} } {m + 1} \paren {\frac a {x^2 + a^2} } \rd x
      | c = Integration by Parts
}}
{{eqn | r = \frac {x^{m + 1} } {m + 1} \arctan \frac x a - \frac a {m + 1} \int \frac {x^{m + 1} \rd x} {x^2 + a^2}
      | c = Primitive of Constant Multiple of Function
}}
{{end-eqn}}
{{qed}}