avewright/proofwiki-math huggingface dataset:
Theorem: Primitive of Reciprocal of q plus p by Secant of a x

:$\ds \int \frac {\d x} {q + p \sec a x} = \frac x q - \frac p q \int \frac {\d x} {p + q \cos a x} + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {q + p \sec a x}
      | r = \frac 1 q \int \frac {q \rd x} {q + p \sec a x}
      | c = multiplying top and bottom by $q$
}}
{{eqn | r = \frac 1 q \int \frac {\paren {q + p \sec a x - p \sec a x} \rd x} {q + p \sec a x}
      | c = 
}}
{{eqn | r = \frac 1 q \int \frac {\paren {q + p \sec a x} \rd x} {q + p \sec a x} - \frac p q \int \frac {\sec a x \rd x} {q + p \sec a x}
      | c = Linear Combination of Primitives
}}
{{eqn | r = \frac 1 q \int \d x - \frac p q \int \frac {\sec a x \rd x} {q + p \sec a x}
      | c = simplifying
}}
{{eqn | r = \frac x q - \frac p q \int \frac {\sec a x \rd x} {q + p \sec a x} + C
      | c = Primitive of Constant
}}
{{eqn | r = \frac x q - \frac p q \int \frac {\cos a x \sec a x \rd x} {q \cos a x + p \cos a x \sec a x} + C
      | c = multiplying top and bottom by $\cos a x$
}}
{{eqn | r = \frac x q - \frac p q \int \frac {\d x} {p + q \cos a x} + C
      | c = Secant is Reciprocal of Cosine
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Cube of Cosecant of a x

:$\ds \int \csc^3 a x \rd x = \frac {-\csc a x \cot a x} {2 a} + \frac 1 {2 a} \ln \size {\tan \dfrac {a x} 2} + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \csc^3 x \rd x
      | r = \frac {-\csc a x \cot a x} {2 a} + \frac 1 2 \int \csc a x \rd x
      | c = Primitive of $\csc^n a x$ where $n = 3$
}}
{{eqn | r = \frac {-\csc a x \cot a x} {2 a} + \frac 1 2 \paren {\frac 1 a \ln \size {\tan \dfrac {a x} 2} }
      | c = Primitive of $\csc a x$: Tangent Form
}}
{{eqn | r = \frac {-\csc a x \cot a x} {2 a} + \frac 1 {2 a} \ln \size {\tan \dfrac {a x} 2} + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of Cosecant of a x

:$\ds \int \frac {\d x} {\csc a x} = \frac {-\cos a x} a + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {\csc a x}
      | r = \int \sin a x \rd x
      | c = Cosecant is Reciprocal of Sine
}}
{{eqn | r = \frac {-\cos a x} a + C
      | c = Primitive of $\sin a x$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of x by Cosecant of a x

:$\ds \int x \csc a x \rd x = \frac 1 {a^2} \paren {a x + \frac {\paren {a x}^3} {18} + \frac {7 \paren {a x}^5} {1800} + \cdots + \frac {\paren {-1}^{n - 1} 2 \paren {2^{2 n - 1} - 1} B_{2n} \paren {a x}^{2 n + 1} } {\paren {2 n + 1}!} + \cdots} + C$
where $B_{2 n}$ is the $2 n$th Bernoulli number.

Proof:
{{begin-eqn}}
{{eqn 	| l = \int x \csc a x \rd x 
	| r = \frac 1 {a^2} \int \theta \csc \theta \rd \theta 
	| c = Substitution of $a x \to \theta$
}}
{{eqn 	| r = \frac 1 {a^2} \int \theta \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^{n - 1} 2 \paren {2^{2 n - 1} - 1} B_{2 n} \, \theta^{2 n - 1} } {\paren {2 n}!} \rd \theta
	| c = Power Series Expansion for Cosecant Function
}}
{{eqn 	| r = \frac 1 {a^2} \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^{n - 1} 2 \paren {2^{2 n - 1} - 1} B_{2 n} } {\paren {2 n}!} \int \theta^{2 n} \rd \theta
	| c = Power Series is Termwise Integrable within Radius of Convergence
}}
{{eqn 	| r = \frac 1 {a^2} \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^{n - 1} 2 \paren {2^{2 n - 1} - 1} B_{2 n} \paren {a x}^{2 n + 1} } {\paren {2 n + 1}!}  + C
	| c = Substituting back $\theta \to ax$
}} 
{{end-eqn}}
{{qed}}
Theorem: Primitive of Cosecant of a x over x

:$\ds \int \frac {\csc a x} x \rd x = \frac {-1} {a x} + \frac {a x} 6 + \frac {7 \paren {a x}^3} {1080} + \cdots + \frac {\paren {-1}^{n - 1} 2 \paren {2^{2 n - 1} - 1} B_{2 n} \paren {a x}^{2 n - 1} } {\paren {2 n - 1} \paren {2 n}!} + \cdots + C$
where $B_n$ is the $n$th Bernoulli number.

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\csc a x} x \rd x
      | r = \int \frac 1 x \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^{n - 1} 2 \paren {2^{2 n - 1} - 1} B_{2 n} \paren {a x}^{2 n - 1} } {\paren {2 n}!} \rd x
      | c = Power Series Expansion for Cosecant Function
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^{n - 1} 2 \paren {2^{2 n - 1} - 1} B_{2 n} a^{2 n - 1} } {\paren {2 n}!} \int  x^{2 n - 2} \rd x
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^{n - 1} 2 \paren {2^{2 n - 1} - 1} B_{2 n} a^{2 n - 1} } {\paren {2 n}!} \paren {\frac {x^{2 n - 1} } {2 n - 1} } + C
      | c = Primitive of Power
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^{n - 1} 2 \paren {2^{2 n - 1} - 1} B_{2 n} \paren {a x}^{2 n - 1} } {\paren {2 n - 1} \paren {2 n}!} + C
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of x by Square of Cosecant of a x

:$\ds \int x \csc^2 a x \rd x = \frac {-x \cot a x} a + \frac  1 {a^2} \ln \size {\sin a x} + 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 = x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = 1
      | c = Derivative of Identity Function
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = \csc^2 a x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {-\cot a x} a
      | c = Primitive of $\csc^2 a x$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int x \csc^2 a x \rd x
      | r = \frac {-x \cot a x} a - \int \frac {-\cot a x} a \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = \frac {-x \cot a x} a + \frac 1 a \int \cot a x \rd x + C
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \frac {-x \cot a x} a + \frac 1 a \paren {\frac 1 a \ln \size {\sin a x} } + C
      | c = Primitive of $\cot a x$
}}
{{eqn | r = \frac {-x \cot a x} a + \frac  1 {a^2} \ln \size {\sin a x} + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of q plus p by Cosecant of a x

:$\ds \int \frac {\d x} {q + p \csc a x} = \frac x q - \frac p q \int \frac {\d x} {p + q \sin a x} + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {q + p \csc a x}
      | r = \frac 1 q \int \frac {q \rd x} {q + p \csc a x}
      | c = multiplying top and bottom by $q$
}}
{{eqn | r = \frac 1 q \int \frac {\paren {q + p \csc a x - p \csc a x} \rd x} {q + p \csc a x}
      | c = 
}}
{{eqn | r = \frac 1 q \int \frac {\paren {q + p \csc a x} \rd x} {q + p \csc a x} - \frac p q \int \frac {\csc a x \rd x} {q + p \csc a x}
      | c = Linear Combination of Primitives
}}
{{eqn | r = \frac 1 q \int \d x - \frac p q \int \frac {\csc a x \rd x} {q + p \csc a x}
      | c = simplifying
}}
{{eqn | r = \frac x q - \frac p q \int \frac {\csc a x \rd x} {q + p \csc a x} + C
      | c = Primitive of Constant
}}
{{eqn | r = \frac x q - \frac p q \int \frac {\sin a x \, \csc a x \rd x} {q \sin a x + p \sin a x \, \csc a x} + C
      | c = multiplying top and bottom by $\sin a x$
}}
{{eqn | r = \frac x q - \frac p q \int \frac {\d x} {p + q \sin a x} + C
      | c = Cosecant is Reciprocal of Sine
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Arcsine of x over a

:$\ds \int \arcsin \frac x a \rd x = x \arcsin \frac x a + \sqrt {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 \frac x a \rd x
      | r = \frac 1 {1 / a} \paren {\frac x a \arcsin \frac x a + \sqrt {1 - \paren {\dfrac x a}^2} } + C
      | c = Primitive of Function of Constant Multiple
}}
{{eqn | r = x \arcsin \frac x a + \sqrt {a^2 - x^2} + C
      | c = after simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Arcsine of x over a

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

Proof:
Let:
{{begin-eqn}}
{{eqn | l = u
      | r = \arcsin \frac x a
      | c = 
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = \sin u 
      | r = \frac x a
      | c = {{Defof|Real Arcsine}}
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = \cos u 
      | r = \sqrt {1 - \frac {x^2} {a^2} }
      | c = Sum of Squares of Sine and Cosine
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \arcsin \frac x a \rd x
      | r = a \int u \cos u \rd u
      | c = Primitive of Function of Arcsine
}}
{{eqn | r = a \paren {\cos u + u \sin u} + C
      | c = Primitive of $x \cos a x$
}}
{{eqn | r = a \paren {\cos u + u \frac x a} + C
      | c = Substitution for $\sin u$ from $\paren 1$
}}
{{eqn | r = a \paren {\sqrt {1 - \frac {x^2} {a^2} } + u \frac x a} + C
      | c = Substitution for $\cos u$ from $\paren 2$
}}
{{eqn | r = a \paren {\sqrt {1 - \frac {x^2} {a^2} } + \frac x a \arcsin \frac x a} + C
      | c = Substitution for $u$
}}
{{eqn | r = x \arcsin \frac x a + \sqrt {a^2 - x^2} + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Arcsine of x over a

:$\ds \int \arcsin \frac x a \rd x = x \arcsin \frac x a + \sqrt {a^2 - x^2} + 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 = \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 = 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = x
      | c = Primitive of Constant
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \arcsin \frac x a \rd x
      | r = x \arcsin \frac x a - \int x \paren {\frac 1 {\sqrt {a^2 - x^2} } } \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = x \arcsin \frac x a - \int \frac {x \rd x} {\sqrt {a^2 - x^2} } + C
      | c = simplifying
}}
{{eqn | r = x \arcsin \frac x a - \paren {-\sqrt {a^2 - x^2} } + C
      | c = Primitive of $\dfrac x {\sqrt {a^2 - x^2} }$
}}
{{eqn | r = x \arcsin \frac x a + \sqrt {a^2 - x^2} + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of x by Arcsine of x over a

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

Proof:
Let:
{{begin-eqn}}
{{eqn | l = u
      | r = \arcsin \frac x a
      | c = 
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = \sin u 
      | r = \frac x a
      | c = {{Defof|Real Arcsine}}
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = \cos u 
      | r = \sqrt {1 - \frac {x^2} {a^2} }
      | c = Sum of Squares of Sine and Cosine
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int x \arcsin \frac x a \rd x
      | r = a \int u \paren {a \sin u} \cos u \rd u
      | c = Primitive of Function of Arcsine
}}
{{eqn | r = a \int a u \frac {\sin 2 u} 2 \rd u
      | c = Double Angle Formula for Sine
}}
{{eqn | r = \frac {a^2} 2 \int u \sin 2 u \rd u
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \frac {a^2} 2 \paren {\frac {\sin 2 u} 4 - \frac {u \cos 2 u} 2} + C
      | c = Primitive of $x \sin a x$ where $a = 2$
}}
{{eqn | r = \frac {a^2 \sin 2 u} 8 - \frac {a^2 u \cos 2 u} 4 + C
      | c = simplifying
}}
{{eqn | r = \frac {a^2 \sin u \cos u} 4 - \frac {a^2 u \cos 2 u} 4 + C
      | c = Double Angle Formula for Sine
}}
{{eqn | r = \frac {a^2 \sin u \cos u} 4 - \frac {a^2 u \paren {\cos^2 u - \sin^2 u} } 4 + C
      | c = Double Angle Formula for Cosine
}}
{{eqn | r = \frac {a^2 \sin u \cos u} 4 - \frac {a^2 \arcsin \frac x a \paren {\cos^2 u - \sin^2 u} } 4 + C
      | c = substituting for $u$
}}
{{eqn | r = \frac {a^2 \frac x a \cos u} 4 - \frac {a^2 \arcsin \frac x a \paren {\cos^2 u - \frac {x^2} {a^2} } } 4 + C
      | c = substituting for $\sin u$ from $(1)$
}}
{{eqn | r = \frac {a^2 \frac x a \sqrt {1 - \frac {x^2} {a^2} } } 4 - \frac {a^2 \arcsin \frac x a \paren {\paren {1 - \frac {x^2} {a^2} } - \frac {x^2} {a^2} } } 4 + C
      | c = substituting for $\cos u$ from $(2)$
}}
{{eqn | r = \paren {\frac {x^2} 2 - \frac {a^2} 4} \arcsin \frac x a + \frac {x \sqrt {a^2 - x^2} } 4 + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of x by Arcsine of x over a

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

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

:$\ds \int \dfrac 1 {x^2} \arcsin \frac x a \rd x = -\frac 1 x \arcsin \frac x a - \frac 1 a \map \ln {\frac {a + \sqrt {a^2 - x^2} } x} + 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 = \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 = \frac 1 {x^2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {-1} x
      | c = Primitive of Power
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \frac 1 {x^2} \arcsin \frac x a \rd x
      | r = \arcsin \frac x a \paren {\frac {-1} x} - \int \paren {\frac {-1} x} \paren {\frac 1 {\sqrt {a^2 - x^2} } } \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = -\frac 1 x \arcsin \frac x a + \int \frac {\d x} {x \sqrt {a^2 - x^2} } \rd x + C
      | c = simplifying
}}
{{eqn | r = -\frac 1 x \arcsin \frac x a - \frac 1 a \map \ln {\frac {a + \sqrt {a^2 - x^2} } x} + C
      | c = Primitive of $\dfrac 1 {x \sqrt {a^2 - x^2} }$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Square of Arcsine of x over a

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

Proof:
Let:
{{begin-eqn}}
{{eqn | l = u
      | r = \arcsin \frac x a
      | c = 
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = \sin u 
      | r = \frac x a
      | c = {{Defof|Real Arcsine}}
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = \cos u 
      | r = \sqrt {1 - \frac {x^2} {a^2} }
      | c = Sum of Squares of Sine and Cosine
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \paren {\arcsin \frac x a}^2 \rd x
      | r = a \int u^2 \cos u \rd x
      | c = Primitive of Function of Arcsine
}}
{{eqn | r = a \paren {2 u \cos u + \paren {u^2 - 2} \sin u} + C
      | c = Primitive of $x^2 \cos a x$
}}
{{eqn | r = a \paren {2 \arcsin \frac x a \sqrt {1 - \frac {x^2} {a^2} } + \paren {\paren {\arcsin \frac x a}^2 - 2} \frac x a} + C
      | c = substituting for $u$, $\sin u$ and $\cos u$
}}
{{eqn | r = x \paren {\arcsin \frac x a}^2 - 2 x + 2 \sqrt{a^2 - x^2} \arcsin \frac x a + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Arccosine of x over a

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

Proof:
Let:
{{begin-eqn}}
{{eqn | l = u
      | r = \arccos \frac x a
      | c = 
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = \cos u 
      | r = \frac x a
      | c = {{Defof|Real Arccosine}}
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = \cos u 
      | r = \sqrt {1 - \frac {x^2} {a^2} }
      | c = Sum of Squares of Sine and Cosine
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \arccos \frac x a \rd x
      | r = -a \int u \sin u \rd u
      | c = Primitive of Function of Arccosine
}}
{{eqn | r = -a \paren {\sin u - u \cos u} + C
      | c = Primitive of $x \sin a x$
}}
{{eqn | r = -a \paren {\sin u - u \frac x a} + C
      | c = Substitution for $\cos u$ from $(1)$
}}
{{eqn | r = -a \paren {\sqrt {1 - \frac {x^2} {a^2} } - u \frac x a} + C
      | c = Substitution for $\sin u$ from $(2)$
}}
{{eqn | r = -a \paren {\sqrt {1 - \frac {x^2} {a^2} } - \frac x a \arccos \frac x a} + C
      | c = Substitution for $u$
}}
{{eqn | r = x \arccos \frac x a - \sqrt {a^2 - x^2} + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Arccosine of x over a

:$\ds \int \arccos \frac x a \rd x = x \arccos \frac x a - \sqrt {a^2 - x^2} + 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 = \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 = 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = x
      | c = Primitive of Constant
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \arccos \frac x a \rd x
      | r = x \arccos \frac x a - \int x \paren {\frac {-1} {\sqrt {a^2 - x^2} } } \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = x \arccos \frac x a + \int \frac {x \rd x} {\sqrt {a^2 - x^2} } + C
      | c = simplifying
}}
{{eqn | r = x \arccos \frac x a + \paren {-\sqrt {a^2 - x^2} } + C
      | c = Primitive of $\dfrac x {\sqrt {a^2 - x^2} }$
}}
{{eqn | r = x \arccos \frac x a - \sqrt {a^2 - x^2} + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Arccosine of x over a

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

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

:$\ds \int x \arccos \frac x a \rd x = \paren {\frac {x^2} 2 - \frac {a^2} 4} \arccos \frac x a - \frac {x \sqrt {a^2 - x^2} } 4 + C$

Proof:
Let:
{{begin-eqn}}
{{eqn | l = u
      | r = \arccos \frac x a
      | c = 
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = \cos u 
      | r = \frac x a
      | c = {{Defof|Real Arccosine}}
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = \sin u 
      | r = \sqrt {1 - \frac {x^2} {a^2} }
      | c = Sum of Squares of Sine and Cosine
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int x \arccos \frac x a \rd x
      | r = -a \int u \left({a \cos u}\right) \sin u \rd u
      | c = Primitive of Function of Arcsine
}}
{{eqn | r = -a \int a u \frac {\sin 2 u} 2 \rd u
      | c = Double Angle Formula for Sine
}}
{{eqn | r = -\frac {a^2} 2 \int u \sin 2 u \rd u
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = -\frac {a^2} 2 \paren {\frac {\sin 2 u} 4 - \frac {u \cos 2 u} 2} + C
      | c = Primitive of $x \sin a x$ where $a = 2$
}}
{{eqn | r = -\frac {a^2 \sin 2 u} 8 + \frac {a^2 u \cos 2 u} 4 + C
      | c = simplifying
}}
{{eqn | r = -\frac {a^2 \sin u \cos u} 4 + \frac {a^2 u \cos 2 u} 4 + C
      | c = Double Angle Formula for Sine
}}
{{eqn | r = -\frac {a^2 \sin u \cos u} 4 + \frac {a^2 u \paren {\cos^2 u - \sin^2 u} } 4 + C
      | c = Double Angle Formula for Cosine
}}
{{eqn | r = -\frac {a^2 \sin u \cos u} 4 + \frac {a^2 \arccos \frac x a \paren {\cos^2 u - \sin^2 u} } 4 + C
      | c = substituting for $u$
}}
{{eqn | r = -\frac {a^2 \sin u \frac x a} 4 + \frac {a^2 \arccos \frac x a \paren {\frac {x^2} {a^2} - \sin^2 u} } 4 + C
      | c = substituting for $\cos u$ from $(1)$
}}
{{eqn | r = -\frac {a^2 \sqrt {1 - \frac {x^2} {a^2} } \frac x a} 4 + \frac {a^2 \arccos \frac x a \paren {\frac {x^2} {a^2} - \paren {1 - \frac {x^2} {a^2} } } } 4 + C
      | c = substituting for $\sin u$ from $(2)$
}}
{{eqn | r = \paren {\frac {x^2} 2 - \frac {a^2} 4} \arccos \frac x a - \frac {x \sqrt {a^2 - x^2} } 4 + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}