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

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

Proof:
{{begin-eqn}}
{{eqn | l = \int x^3 \paren {\sqrt {x^2 - a^2} }^3 \rd x
      | r = \int x \paren {x^2} \paren {\sqrt {x^2 - a^2} }^3 \rd x
      | c = 
}}
{{eqn | r = \int x \paren {x^2 - a^2 + a^2} \paren {\sqrt {x^2 - a^2} }^3 \rd x
      | c = Primitive of Power
}}
{{eqn | r = \int x \paren {x^2 - a^2} \paren {\sqrt {x^2 - a^2} }^3 \rd x + a^2 \int x \paren {\sqrt {x^2 - a^2} }^3 \rd x
      | c = Linear Combination of Primitives
}}
{{eqn | r = \int x \paren {\sqrt {x^2 - a^2} }^5 \rd x + a^2 \int x \paren {\sqrt {x^2 - a^2} }^3 \rd x
      | c = simplifying
}}
{{end-eqn}}
Let:
{{begin-eqn}}
{{eqn | l = z
      | r = x^2 - a^2
}}
{{eqn | ll= \leadsto
      | l = \frac {\d z} {\d x}
      | r = 2 x
      | c = Power Rule for Derivatives
}}
{{eqn | ll= \leadsto
      | o = 
      | r = \int x \paren {\sqrt {x^2 - a^2} }^5 \rd x + a^2 \int x \paren {\sqrt {x^2 - a^2} }^3 \rd x
      | c = 
}}
{{eqn | r = \int \frac {\sqrt z z^{5/2} } {2 \sqrt z} \rd z + a^2 \int \frac {\sqrt z z^{3/2} } {2 \sqrt z} \rd z
      | c = Integration by Substitution
}}
{{eqn | r =  \frac 1 2 \int z^{5/2} \rd z + \frac {a^2} 2 \int z^{3/2} \rd z
      | c = simplifying
}}
{{eqn | r = \frac 1 2 \frac {z^{7/2} } {7/2} + \frac {a^2} 2 \frac {z^{5/2} } {5/2} + C
      | c = Primitive of Power
}}
{{eqn | r = \frac {z^{7/2} } 7 + a^2 \frac {z^{5/2} } 5 + C
      | c = simplifying
}}
{{eqn | r = \frac {\paren {\sqrt {x^2 - a^2} }^7} 7 + \frac {a^2 \paren {\sqrt {x^2 - a^2} }^5} 5 + C
      | c = substituting for $z$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Root of x squared minus a squared cubed over x

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

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 {\paren {\sqrt {x^2 - a^2} }^3} x \rd x
      | r = \int \frac {\paren {\sqrt {z - a^2} }^3} {2 z} \rd z
      | c = Integration by Substitution
}}
{{eqn | r = \frac {\paren {\sqrt {z - a^2} }^3} 3 - \frac {a^2} 2 \int \frac {\sqrt {z - a^2} } z \rd z
      | c = Primitive of $\dfrac {\paren {\sqrt {a x + b} }^m} x$
}}
{{eqn | r = \frac {\paren {\sqrt {z - a^2} }^3} 3 - \frac {a^2} 2 \paren {2 \sqrt {z - a^2} - a^2 \int \frac {\d z} {z \sqrt {z - a^2} } }
      | c = Primitive of $\dfrac {\sqrt {a x + b} } x$
}}
{{eqn | r = \frac {\paren {\sqrt {x^2 - a^2} }^3} 3 - a^2 \sqrt {x^2 - a^2} + a^4 \int \frac {\d x} {x \sqrt {x^2 - a^2} }
      | c = substituting for $z$ and simplifying
}}
{{eqn | r = \frac {\paren {\sqrt {x^2 - a^2} }^3} 3 - a^2 \sqrt {x^2 - a^2} + a^3 \arcsec \size {\frac x a} + C
      | c = Primitive of $\dfrac 1 {x \sqrt {x^2 - a^2} }$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Root of x squared minus a squared cubed over x squared

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

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 {\paren {\sqrt {x^2 - a^2} }^3} {x^2} \rd x
      | r = \int \frac {\paren {\sqrt {z - a^2} }^3} {2 z \sqrt z} \rd z
      | c = Integration by Substitution
}}
{{eqn | r = \frac {-\paren {\sqrt {z - a^2} }^3} {\sqrt z} + \frac 3 2 \int \frac {\sqrt {z - a^2} } {\sqrt z} \rd z
      | c = Primitive of $\dfrac {\paren {a x + b}^m} {\paren {p x + q}^n}$: Formulation 3
}}
{{eqn | r = \frac {-\paren {\sqrt {x^2 - a^2} }^3} x + 3 \int \sqrt {x^2 - a^2} \rd x
      | c = substituting for $z$ and simplifying
}}
{{eqn | r = \frac {-\paren {\sqrt {x^2 - a^2} }^3} x - \frac {3 x \sqrt {x^2 - a^2} } 2 - \frac {3 a^2} 2 \ln \size {x + \sqrt {x^2 - a^2} } + C
      | c = Primitive of $\sqrt {x^2 - a^2}$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Root of x squared minus a squared cubed over x cubed

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

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 {\paren {\sqrt {x^2 - a^2} }^3} {x^3} \rd x
      | r = \int \frac {\paren {\sqrt {z - a^2} }^3} {2 z^2} \rd z
      | c = Integration by Substitution
}}
{{eqn | r = \frac 1 2 \paren {\frac {-\paren {\sqrt {z - a^2} }^3} z + \frac 3 2 \int \frac {\sqrt {z - a^2} } z \rd z}
      | c = Primitive of $\dfrac {\paren {a x + b}^m} {\paren {p x + q}^n}$: Formulation 3
}}
{{eqn | r = \frac {-\paren {\sqrt {x^2 - a^2} }^3} {2 x^2} + \frac 3 2 \int \frac {\sqrt {x^2 - a^2} } x \rd x
      | c = substituting for $z$ and simplifying
}}
{{eqn | r = \frac {-\paren {\sqrt {x^2 - a^2} }^3} {2 x^2} + \frac 3 2 \paren {\sqrt {x^2 - a^2} - a \arcsec \size {\frac x a} } + C
      | c = Primitive of $\dfrac {\sqrt {x^2 - a^2} } x$
}}
{{eqn | r = \frac {-\paren {\sqrt {x^2 - a^2} }^3} {2 x^2} + \frac {3 \sqrt {x^2 - a^2} } 2 - \frac {3 a} 2 \arcsec \size {\frac x a} + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of x over Root of a squared minus x squared

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

Proof:
Let:
{{begin-eqn}}
{{eqn | l = z^2
      | r = a^2 - x^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 2 z \frac {\d z} {\d x}
      | r = -2 x
      | c = Chain Rule for Derivatives, Power Rule for Derivatives
}}
{{eqn | ll= \leadsto
      | l = \int \frac {x \rd x} {\sqrt {a^2 - x^2} }
      | r = \int -\frac {z \rd z} z
      | c = Integration by Substitution
}}
{{eqn | r = -\int \rd z
      | c = 
}}
{{eqn | r = -z + C
      | c = Primitive of Constant
}}
{{eqn | r = -\sqrt {a^2 - x^2} + C
      | c = substituting for $z$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of x cubed over Root of a squared minus x squared

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

Proof:
With a view to expressing the problem 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^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = 2 x
      | c = Power Rule for Derivatives
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = \frac x {\sqrt {a^2 - x^2} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = -\sqrt {a^2 - x^2}
      | c = Primitive of $\dfrac x {\sqrt {a^2 - x^2} }$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \frac {x^3 \rd x} {\sqrt {a^2 - x^2} }
      | r = \int x^2 \frac {x \rd x} {\sqrt {a^2 - x^2} }
      | c = 
}}
{{eqn | r = -x^2 \sqrt {a^2 - x^2} - \int 2 x \paren {-\sqrt {a^2 - x^2} } \rd x
      | c = Integration by Parts
}}
{{eqn | r = -x^2 \sqrt {a^2 - x^2} + 2 \int x \paren {\sqrt {a^2 - x^2} } \rd x
      | c = simplification
}}
{{eqn | r = -x^2 \sqrt {a^2 - x^2} + 2 \paren {-\frac {\paren {\sqrt {a^2 - x^2} }^3} 3} + C
      | c = Primitive of $x \sqrt {a^2 - x^2}$
}}
{{eqn | r = \paren {a^2 - x^2 - a^2} \sqrt {a^2 - x^2} - \frac {2 \paren {\sqrt {a^2 - x^2} }^3} 3 + C
      | c = 
}}
{{eqn | r = \paren {\sqrt {a^2 - x^2} }^3 - a^2 \sqrt {a^2 - x^2} - \frac {2 \paren {\sqrt {a^2 - x^2} }^3} 3 + C
      | c = 
}}
{{eqn | r = \frac {\paren {\sqrt {a^2 - x^2} }^3} 3 - a^2 \sqrt {a^2 - x^2} + C
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of x squared by Root of a squared minus x squared

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

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 {\d x} {x^2 \sqrt {a^2 - x^2} }
      | r = \int \frac {\d z} {2 z \sqrt z \sqrt {a^2 - z} }
      | c = Integration by Substitution
}}
{{eqn | r = \frac 1 2 \int \frac {\d z} {z^{3/2} \sqrt {a^2 - z} }
      | c = 
}}
{{end-eqn}}
Using Primitive of $ \dfrac 1 {x^m \sqrt {a x + b} }$:
:$\ds \int \frac {\d x} {x^m \sqrt {a x + b} } = -\frac {\sqrt {a x + b} } {\paren {m - 1} b x^{m - 1} } - \frac {\paren {2 m - 3} a} {\paren {2 m - 2} b} \int \frac {\d x} {x^{m - 1} \sqrt {a x + b} }$
Setting:
{{begin-eqn}}
{{eqn | l = x
      | o = :=
      | r = -z
}}
{{eqn | l = m
      | o = :=
      | r = \frac 3 2
}}
{{eqn | l = a
      | o = :=
      | r = 1
}}
{{eqn | l = b
      | o = :=
      | r = a^2
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \frac 1 2 \int \frac {\d z} {\paren {-z}^{3/2} \sqrt {-z + a^2} }
      | r = \frac {-\sqrt {-z + a^2} } {2 \paren {\paren {\frac 3 2} - 1} a^2 \paren {-z}^{\paren {3/2} - 1} } - \frac {2 \paren {\frac 3 2} - 3} {2 \paren {2 \paren {\frac 3 2} - 2} a^2} \int \frac {\d z} {\paren {-z}^{\paren {\frac 3 2} - 1} \sqrt {-z + a^2} } + C
      | c = Primitive of $ \dfrac 1 {x^m \sqrt {a x + b} }$
}}
{{eqn | r = \frac {-\sqrt {a^2 - z} } {a^2 z^{1/2} } - 0 + C
      | c = simplifying
}}
{{eqn | r = \frac {-\sqrt {a^2 - x^2} } {a^2 x} + C
      | c = substituting back for $z$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of x cubed by Root of a squared minus x squared

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

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 {\d x} {x^3 \sqrt {a^2 - x^2} }
      | r = \int \frac {\d z} {2 z^{3/2} \sqrt z \sqrt {a^2 - z} }
      | c = Integration by Substitution
}}
{{eqn | r = \frac 1 2 \int \frac {\d z} {z^2 \sqrt {-z + a^2} }
      | c = 
}}
{{end-eqn}}
Using Primitive of $ \dfrac 1{x^m \sqrt{a x + b} }$:
:$\ds \int \frac {\d x} {x^m \sqrt {a x + b} } = -\frac {\sqrt{a x + b} } {\paren {m - 1} b x^{m - 1} } - \frac {\paren {2 m - 3} a} {\paren {2 m - 2} b} \int \frac {\d x} {x^{m - 1} \sqrt{a x + b} }$
Setting:
{{begin-eqn}}
{{eqn | l = x
      | o = :=
      | r = z
}}
{{eqn | l = m
      | o = :=
      | r = 2
}}
{{eqn | l = a
      | o = :=
      | r = -1
}}
{{eqn | l = b
      | o = :=
      | r = a^2
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \frac 1 2 \int \frac {\d z} {z^2 \sqrt {-z + a^2} }
      | r = \frac {-\sqrt {-z + a^2} } {2 \paren {2 - 1} a^2 z^{2 - 1} } - \frac {\paren {2 \paren 2 - 3} \paren {-1} } {2 \paren {2 \paren 2 - 2} a^2} \int \frac {\d z} {z^{2 - 1} \sqrt {-z + a^2} } + C
      | c = Primitive of $ \dfrac 1{x^m \sqrt{a x + b} }$
}}
{{eqn | r = \frac {-\sqrt {a^2 - z} } {2 a^2 z} - \frac 1 {4 a^2} \int \frac {\d z} {z \sqrt{a^2 - z} } + C
      | c = simplifying
}}
{{eqn | r = \frac {-\sqrt {a^2 - x^2} } {2 a^2 x^2} + \frac 1 {4 a^2} \paren {\int \frac {2 x \rd x} {x^2 \sqrt {a^2 - x^2} } } + C
      | c = substituting for $z$
}}
{{eqn | r = \frac {-\sqrt {a^2 - x^2} } {2 a^2 x^2} + \frac 1 {2 a^2} \paren {\int \frac {\d x} {x \sqrt {a^2 - x^2} } } + C
      | c = simplification
}}
{{eqn | r =\frac {-\sqrt {a^2 - x^2} } {2 a^2 x^2} + \frac 1 {2 a^3} \paren {-\map \ln {\frac {a + \sqrt {a^2 - x^2} } {\size x} } } + C
      | c = Primitive of $\dfrac 1 {x \sqrt {a^2 - x^2} }$
}}
{{eqn | r =\frac {-\sqrt {a^2 - x^2} } {2 a^2 x^2} - \frac 1 {2 a^3} \map \ln {\frac {a + \sqrt {a^2 - x^2} } {\size x} } + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Root of a squared minus x squared/Arcsine Form

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

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 = a^2 - x^2
      | r = a^2 - a^2 \sin^2 \theta
      | c = 
}}
{{eqn | r = a^2 \paren {1 - \sin^2 \theta}
      | c = 
}}
{{eqn | r = a^2 \cos^2 \theta
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = \sqrt {a^2 - x^2}
      | r = a \cos \theta
      | c = 
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = x
      | r = a \sin \theta
}}
{{eqn | n = 3
      | ll= \leadsto
      | l = \theta
      | r = \map \arcsin {\frac x a}
      | c = {{Defof|Real Arcsine}}
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \int \sqrt {a^2 - x^2} \rd x
      | r = \int \sqrt {a^2 - x^2} \, a \cos \theta \rd \theta
      | c = Integration by Substitution from $(1)$
}}
{{eqn | r = \int a^2 \cos^2 \theta \rd \theta
      | c = substituting for $\sqrt {a^2 - x^2}$ from $(2)$
}}
{{eqn | r = a^2 \int \cos^2 \theta \rd \theta
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = a^2 \frac {\sin \theta \cos \theta + \theta} 2 + C
      | c = {{Corollary|Primitive of Square of Cosine Function}}
}}
{{eqn | r = \frac 1 2 a \sin \theta \, a \cos \theta + \frac {a^2 \theta} 2 + C
      | c = rearranging
}}
{{eqn | r = \frac 1 2 x a \cos \theta + \frac {a^2 \theta} 2 + C
      | c = substituting $x = a \sin \theta$
}}
{{eqn | r = \frac 1 2 x \sqrt {a^2 - x^2} + \frac {a^2 \theta} 2 + C
      | c = substituting $\sqrt {a^2 - x^2} = a \cos \theta$ from $(2)$
}}
{{eqn | r = \frac {x \sqrt {a^2 - x^2} } 2 + \frac {a^2} 2 \map \arcsin {\frac x a} + C
      | c = substituting for $\theta = \map \arcsin {\dfrac x a}$ from $(3)$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of x by Root of a squared minus x squared

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

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 x \sqrt {a^2 - x^2} \rd x
      | r = \int \frac {\sqrt z \sqrt {a^2 - z} \rd z} {2 \sqrt z}
      | c = Integration by Substitution
}}
{{eqn | r = \frac 1 2 \int \sqrt {a^2 - z} \rd z
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \frac 1 2 \frac {2 \paren {\sqrt {a^2 - z} }^3} {-3} + C
      | c = Primitive of $\sqrt {a x + b}$
}}
{{eqn | r = \frac {-\paren {\sqrt {a^2 - x^2} }^3} 3 + C
      | c = substituting for $z$ and simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of x squared by Root of a squared minus x squared

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

Proof:
Let us assume that $a > 0$.
Let:
{{begin-eqn}}
{{eqn | l = x
      | r = a \sin t
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\d x} {\d t}
      | r = a \cos t
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a^2 - x^2
      | r = a^2 - a^2 \sin^2 t
      | c = 
}}
{{eqn | r = a^2 \paren {1 - \sin^2 t}
      | c = 
}}
{{eqn | r = a^2 \cos^2 t
      | c = Sum of Squares of Sine and Cosine
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = \int x^2 \sqrt {a^2 - x^2} \rd x
      | r = \int a^2 \sin^2 t \cdot \sqrt {a^2 \cos^2 t} \cdot a \cos t \rd t
      | c = Integration by Substitution
}}
{{eqn | r = a^4 \int \sin^2 t \cos^2 t \rd t
      | c = simplifying
}}
{{eqn | r = a^4 \paren {\frac t 8 - \frac {\sin 4 t} {32} } + C
      | c = Primitive of $\sin^2 a t \cos^2 a t$ where $a \gets 1$
}}
{{eqn | r = a^4 \paren {\frac t 8 - \dfrac {4 \sin t \cos t - 8 \sin^3 t \cos t} {32} } + C
      | c = Quadruple Angle Formula for Sine
}}
{{eqn | n = 1
      | r = \dfrac {a^4} 8 \paren {t - \sin t \cos t - 2 \sin^3 t \cos t} + C
      | c = simplifying
}}
{{end-eqn}}
Recall:
{{begin-eqn}}
{{eqn | l = x
      | r = a \sin t
      | c = 
}}
{{eqn | ll= \leadsto
      | l = t
      | r = \arcsin \frac x a
      | c = 
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | r = \frac {a^4} 8 \paren {t - \sin t \cos t - 2 \sin^3 t \cos t} + C
      | o = 
      | c = from $(1)$
}}
{{eqn | r = \frac {a^4} 8 \paren {\arcsin \frac x a - \paren {\frac x a} \paren {\frac {\sqrt {a^2 - x^2} } a} + 2 \paren {\frac x a}^3 \paren {\frac {\sqrt {a^2 - x^2} } a} } + C
      | c = substituting $\sin t = \dfrac x a$, $\cos t = \dfrac {\sqrt {a^2 - x^2} } a$
}}
{{eqn | r = \frac {a^4} 8 \paren {\arcsin \frac x a + \paren {\frac x a} \paren {\frac {\sqrt {a^2 - x^2} } a} \paren {-1 + \frac {2 x^2} {a^2} } } + C
      | c = Distributive Laws of Arithmetic
}}
{{eqn | r = \frac {a^4} 8 \paren {\arcsin \frac x a + \paren {\frac x a} \paren {\frac {\sqrt {a^2 - x^2} } a} \paren {\dfrac {-2 a^2 + 2 x^2 + a^2} {a^2} } } + C
      | c = manipulating as necessary
}}
{{eqn | r = \frac {a^4} 8 \paren {\arcsin \frac x a + \paren {\frac x a} \frac {\sqrt {a^2 - x^2} } a \paren {-2 \frac {a^2 - x^2} {a^2} + 1} } + C
      | c = 
}}
{{eqn | r = -\frac {x \paren {\sqrt {a^2 - x^2} }^3} 4 + \frac {a^2 x \sqrt {a^2 - x^2} } 8 + \frac {a^4} 8 \arcsin \frac x a + C
      | c = simplifying and rearranging
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of x cubed by Root of a squared minus x squared

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

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 x^3 \sqrt {a^2 - x^2} \rd x
      | r = \int \frac {z^{3/2} \sqrt {a^2 - z} \rd z} {2 \sqrt z}
      | c = Integration by Substitution
}}
{{eqn | r = \frac 1 2 \int z \sqrt {a^2 - z} \rd z
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \frac 1 2 \paren {\frac {2 \paren {-3 z - 2 a^2} } {15} \paren {\sqrt {a^2 - z} }^3} + C
      | c = Primitive of $x \sqrt {\paren {a x + b} }$
}}
{{eqn | r = \frac {-3 z - 2 a^2} {15} \paren {\sqrt {a^2 - z} }^3 + C
      | c = simplification
}}
{{eqn | r = \frac {-3 x^2 - 2 a^2} {15} \paren {\sqrt {a^2 - x^2} }^3 + C
      | c = substituting for $z$
}}
{{eqn | r = \frac {3 a^2 - 3 x^2 - 5 a^2} {15} \paren {\sqrt {a^2 - x^2} }^3 + C
      | c = 
}}
{{eqn | r = \frac {3 \paren {a^2 - x^2} \paren {\sqrt {a^2 - x^2} }^3 - 5 a^2 \paren {\sqrt {a^2 - x^2} }^3} {15} + C
      | c = 
}}
{{eqn | r = \frac {\paren {\sqrt {a^2 - x^2} }^5} 5 - \frac {a^2 \paren {\sqrt {a^2 - x^2} }^3} 3 + C
      | c = simplification
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Root of a squared minus x squared over x

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

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 {a^2 - x^2} } x \rd x
      | r = \int \frac {\sqrt {a^2 - z} \rd z} {2 \sqrt z \sqrt z}
      | c = Integration by Substitution
}}
{{eqn | r = \frac 1 2 \int \frac {\sqrt {a^2 - z} \rd z} z
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \frac 1 2 \paren {2 \sqrt {a^2 - z} + a^2 \int \frac {\d z} {z \sqrt {a^2 - z} } } + C
      | c = Primitive of $\dfrac {\sqrt {a x + b} } x$
}}
{{eqn | r = \sqrt {a^2 - x^2} + \frac {a^2} 2 \int \frac {2 x \rd x} {x^2 \sqrt {a^2 - x^2} } + C
      | c = substituting for $z$
}}
{{eqn | r = \sqrt {a^2 - x^2} + a^2 \int \frac {\d x} {x \sqrt {a^2 - x^2} } + C
      | c = simplifying
}}
{{eqn | r = \sqrt {a^2 - x^2} - a^2 \paren {-\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} }$
}}
{{eqn | r = \sqrt {a^2 - x^2} - a \map \ln {\frac {a + \sqrt {a^2 - x^2} } x} + C
      | c = simplification
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Root of a squared minus x squared over x squared

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

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 {a^2 - x^2} } {x^2} \rd x
      | r = \int \frac {\sqrt {a^2 - z} \rd z} {2 z \sqrt z}
      | c = Integration by Substitution
}}
{{eqn | r = \frac 1 2 \int \frac {\sqrt {a^2 - z} \rd z} {z^{3/2} }
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \frac 1 2 \paren {\frac {-\sqrt {a^2 - z} } {\frac 1 2 \sqrt z} - \frac 1 2 \int \frac {\d z} {\sqrt z \sqrt {a^2 - z} } } + C
      | c = Primitive of $\dfrac {\sqrt {a x + b} } {x^m}$
}}
{{eqn | r = \frac {-\sqrt {a^2 - x^2} } x - \frac 1 2 \int \frac {2 x \rd x} {x \sqrt {a^2 - x^2} } + C
      | c = substituting for $z$
}}
{{eqn | r = \frac {-\sqrt {a^2 - x^2} } x - \int \frac {\d x} {\sqrt {a^2 - x^2} } + C
      | c = simplifying
}}
{{eqn | r = \frac {-\sqrt {a^2 - x^2} } x - \arcsin \frac x a + C
      | c = Primitive of $\dfrac 1 {\sqrt {a^2 - x^2} }$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Root of a squared minus x squared over x cubed

:$\ds \int \frac {\sqrt {a^2 - x^2} } {x^3} \rd x = \frac {-\sqrt {a^2 - x^2} } {2 x^2} + \frac 1 {2 a} \map \ln {\frac {a + \sqrt {a^2 - x^2} } {\size x} } + C$

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 {a^2 - x^2} } {x^3} \rd x
      | r = \int \frac {\sqrt {a^2 - z} \rd z} {2 z^{3/2} \sqrt z}
      | c = Integration by Substitution
}}
{{eqn | r = \frac 1 2 \int \frac {\sqrt {a^2 - z} \rd z} {z^2}
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \frac 1 2 \paren {\frac {-\sqrt {a^2 - z} } z - \frac 1 2 \int \frac {\d z} {z \sqrt {a^2 - z} } } + C
      | c = Primitive of $\dfrac {\sqrt {a x + b} } {x^m}$
}}
{{eqn | r = \frac {-\sqrt {a^2 - x^2} } {2 x^2} - \frac 1 4 \int \frac {2 x \rd x} {x^2 \sqrt {a^2 - x^2} } + C
      | c = substituting for $z$
}}
{{eqn | r = \frac {-\sqrt {a^2 - x^2} } {2 x^2} - \frac 1 2 \int \frac {\d x} {x \sqrt {a^2 - x^2} } + C
      | c = simplifying
}}
{{eqn | r = \frac {-\sqrt {a^2 - x^2} } {2 x^2} - \frac 1 2 \paren {-\frac 1 a \map \ln {\frac {a + \sqrt {a^2 - x^2} } {\size x} } } + C
      | c = Primitive of $\dfrac 1 {x \sqrt {a^2 - x^2} }$
}}
{{eqn | r = \frac {-\sqrt {a^2 - x^2} } {2 x^2} + \frac 1 {2 a} \map \ln {\frac {a + \sqrt {a^2 - x^2} } {\size x} } + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of x over Root of a squared minus x squared cubed

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

Proof:
Let:
{{begin-eqn}}
{{eqn | l = z
      | r = a^2 - 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 {x \rd x} {\paren {\sqrt {a^2 - x^2} }^3}
      | r = \int \frac {x \rd z} {-2 x z^{3/2} }
      | c = Integration by Substitution
}}
{{eqn | r = \frac 1 2 \int -z^{-3/2} \rd z
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \frac 1 2 \paren {\frac {z^{1/2} } {\frac 1 2} } + C
      | c = Primitive of Power
}}
{{eqn | r = \frac 1 {\sqrt z} + C
      | c = simplifying
}}
{{eqn | r = \frac 1 {\sqrt {a^2 - x^2} } + C
      | c = substituting for $z$
}}
{{end-eqn}}
{{qed}}