avewright/proofwiki-math huggingface dataset:
Theorem: Primitive of Power of x by Arcsine of x

:$\ds \int x^m \arcsin x \rd x = \frac {x^{m + 1} } {m + 1} \arcsin x - \frac 1 {m + 1} \int \frac {x^{m + 1} \rd x} {\sqrt {1 - x^2} }$

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

:$\ds \int x^m \arcsin x \rd x = \frac {x^{m + 1} } {m + 1} \arcsin x - \frac 1 {m + 1} \int \frac {x^{m + 1} \rd x} {\sqrt {1 - x^2} }$

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 of x by Arcsine of x

:$\ds \int x^m \arcsin x \rd x = \frac {x^{m + 1} } {m + 1} \arcsin x - \frac 1 {m + 1} \int \frac {x^{m + 1} \rd x} {\sqrt {1 - x^2} }$

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: Characterization of Compact Element in Complete Lattice/Statement 1 implies Statement 3

Let $L = \struct{S, \preceq}$ be a complete lattice.
Let $a \in S$ be a compact element
Then:
:$\forall A \subseteq S : a \preceq \sup A \implies \exists F \subseteq A : F$ is finite $: a \preceq \sup F$

Proof:
Let $A \subseteq S : a \preceq \sup A$.
Let $D = \leftset{b \in A : \exists F \subseteq A : F}$ is finite $\rightset{: b = \sup F}$
==== $D$ is a Directed Subset ====
We show that $D$ is a directed subset.
Let $x, y \in D$.
By definition of $D$:
:$\exists F, G \subseteq A: F, G$ are finite $: x = \sup F, y = \sup G$
Let $H = F \cup G$.
From Union of Finite Sets is Finite:
:$H$ is finite of $A$
Hence:
:$z = \sup H \in D$.
Furthermore:
:$z = \sup \set{x, y}$
By definition of supremum:
:$x, y \preceq z$
Since $x,y$ were arbitrary, then $D$ is a directed subset by definition.
{{qed|lemma}}
==== Supremum of $D$ Equals Supremum of $A$ ====
We show that $\sup D = \sup A$.
Let $x \in D$.
By definition of $D$:
:$\exists F \subseteq A: F$ is finite $: x = \sup F$
From Supremum of Subset:
:$\sup F \preceq \sup A$
Since $x$ was arbitrary, it follows that:
:$\sup A$ is an upper bound for $D$
By definition of supremum:
:$\sup D \preceq \sup A$
Note that for all $b \in A$:
:$b = \sup \set b \in D$
Hence:
:$\sup D$ is an upper bound for $A$
By definition of supremum:
:$\sup A \preceq \sup D$
From {{Ordering-axiom|3}}:
:$\sup A = \sup D$
{{qed|lemma}}
By definition of compact element:
:$\exists d \in D : a \preceq d$
By definition of $D$:
:$\exists F \subseteq A : \sup F = d$
Hence:
:$\exists F \subseteq A : F$ is finite $: a \preceq \sup F$
Since $A$ was arbitrary:
:$\forall A \subseteq S : a \preceq \sup A \implies \exists F \subseteq A : F$ is finite $: a \preceq \sup F$
Theorem: Characterization of Compact Element in Complete Lattice/Statement 3 implies Statement 2

Let $L = \struct{S, \preceq}$ be a complete lattice.
Let $a \in S$ satisfy:
:$\forall A \subseteq S : a \preceq \sup A \implies \exists F \subseteq A : F$ is finite $: a \preceq \sup F$ 
Then:
:$\forall I \subseteq S : I$ is an ideal $: a \preceq \sup I \implies a \in I$

Proof:
Let:
:$I \subseteq S : I$ is an ideal $: a \preceq \sup I$
We have {{Hypothesis}}:
:$\exists F \subseteq I : F$ is finite $: a \preceq \sup F$
By {{Join-semilattice-ideal-axiom|2}}:
:$\sup F \in I$
By {{Join-semilattice-ideal-axiom|1}}:
:$a \in I$
Since $I$ was arbitrary:
:$\forall I \subseteq S : I$ is an ideal $: a \preceq \sup I \implies a \in I$
Theorem: Characterization of Compact Element in Complete Lattice/Statement 2 implies Statement 1

Let $L = \struct{S, \preceq}$ be a complete lattice.
Let $a \in S$ satisfy:
:$\forall I \subseteq S : I$ is an ideal $: a \preceq \sup I \implies a \in I$
Then:
:$a$ is a compact element

Proof:
Let $D$ be a directed subset of $S$:
:$a \preceq \sup D$
Let $I = {b \in S : \exists d \in D : b \preceq d}$.
==== $I$ is an Ideal of $S$ ====
We will show that $I$ satisfies the join semilattice ideal axioms.
===== $I$ is a Lower Section =====
Let $x \in I$.
Let $y \preceq x$.
By definition of $I$:
:$\exists d \in D : x \preceq d$
By {{Ordering-axiom|2}}:
:$y \preceq d$
Hence:
:$y \in I$
It follows that $I$ is a lower section of $S$.
{{qed|lemma}}
===== $I$ is a Join Subsemilattice =====
Let $x, y \in I$.
By definition of $I$:
:$\exists d_1, d_2 \in D : x \preceq d, y \preceq e$
By definition of a directed subset:
:$\exists d \in D : d_1, d_2 \preceq d$
By {{Ordering-axiom|2}}:
:$x, y \preceq d$
By definition of join:
:$x \vee y \preceq d$
Hence:
:$x \vee y \in I$
{{qed|lemma}}
This proves $I$ satisfies the join semilattice ideal axioms.
It follows that $I$ is an ideal by definition.
{{qed|lemma}}
==== Supremum of $I$ Equals Supremum of $D$ ====
We show that $\sup I = \sup D$.
Let $x \in I$.
By definition of $I$:
:$\exists d \in D: x \preceq d$
By definition of supremum:
:$x \preceq \sup D$
Since $x$ was arbitrary, it follows that:
:$\sup D$ is an upper bound for $I$
By definition of supremum:
:$\sup I \preceq \sup D$
Note that for all $d \in D$:
:$d \in I$
Hence:
:$\sup I$ is an upper bound for $D$
By definition of supremum:
:$\sup D \preceq \sup I$
From {{Ordering-axiom|3}}:
:$\sup I = \sup D$
{{qed|lemma}}
We have {{Hypothesis}}:
:$a \in I$
By definition of $I$:
:$\exists d \in D : a \preceq d$
Since $D$ was arbitrary:
:for every directed subset $D$ of $S$ such that $a \preceq \sup D$
::$\exists d \in D: a \preceq d$
Hence $a$ is a compact element by definition.
Theorem: Primitive of Power of x by Arccosine of x

:$\ds \int x^m \arccos x \rd x = \frac {x^{m + 1} } {m + 1} \arccos x + \frac 1 {m + 1} \int \frac {x^{m + 1} \rd x} {\sqrt {1 - x^2} }$

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

:$\ds \int x^m \arccos x \rd x = \frac {x^{m + 1} } {m + 1} \arccos x + \frac 1 {m + 1} \int \frac {x^{m + 1} \rd x} {\sqrt {1 - x^2} }$

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 of x by Arccosine of x

:$\ds \int x^m \arccos x \rd x = \frac {x^{m + 1} } {m + 1} \arccos x + \frac 1 {m + 1} \int \frac {x^{m + 1} \rd x} {\sqrt {1 - x^2} }$

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 of x by Arctangent of x

:$\ds \int x^m \arctan x \rd x = \frac {x^{m + 1} } {m + 1} \arctan x - \frac 1 {m + 1} \int \frac {x^{m + 1} \rd x} {x^2 + 1}$

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

:$\ds \int x^m \arctan x \rd x = \frac {x^{m + 1} } {m + 1} \arctan x - \frac 1 {m + 1} \int \frac {x^{m + 1} \rd x} {x^2 + 1}$

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 of x by Arctangent of x

:$\ds \int x^m \arctan x \rd x = \frac {x^{m + 1} } {m + 1} \arctan x - \frac 1 {m + 1} \int \frac {x^{m + 1} \rd x} {x^2 + 1}$

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}}
Theorem: Primitive of Power of x by Arccotangent of x

:$\ds \int x^m \arccot x \rd x = \frac {x^{m + 1} } {m + 1} \arccot x + \frac 1 {m + 1} \int \frac {x^{m + 1} \rd x} {x^2 + 1}$

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

:$\ds \int x^m \arccot x \rd x = \frac {x^{m + 1} } {m + 1} \arccot x + \frac 1 {m + 1} \int \frac {x^{m + 1} \rd x} {x^2 + 1}$

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 of x by Arccotangent of x

:$\ds \int x^m \arccot x \rd x = \frac {x^{m + 1} } {m + 1} \arccot x + \frac 1 {m + 1} \int \frac {x^{m + 1} \rd x} {x^2 + 1}$

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 of x by Arcsecant of x

:$\ds \int x^m \arcsec x \rd x = \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}$

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

:$\ds \int x^m \arcsec x \rd x = \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}$

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