avewright/proofwiki-math huggingface dataset:
Theorem: Primitive of Power of x by Arccosine of x over a

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

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 over a

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

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 over a

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

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 over a

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

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 over a

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

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 over a

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

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

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

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 of x by Arccosecant of x over a

:<nowiki>$\ds \int x^m \arccsc \frac x a \rd x = \begin {cases}
\ds \dfrac {x^{m + 1} } {m + 1} \arccsc \dfrac x a + \dfrac a {m + 1} \int \dfrac {x^m \rd x} {\sqrt {x^2 - a^2} } & : 0 < \arccsc \dfrac x a < \dfrac \pi 2 \\ \\
\ds \dfrac {x^{m + 1} } {m + 1} \arccsc \dfrac x a - \dfrac a {m + 1} \int \dfrac {x^m \rd x} {\sqrt {x^2 - a^2} } & : -\dfrac \pi 2 < \arccsc \dfrac x a < 0
\end {cases}$</nowiki>

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 of x by Arccosecant of x over a

:<nowiki>$\ds \int x^m \arccsc \frac x a \rd x = \begin {cases}
\ds \dfrac {x^{m + 1} } {m + 1} \arccsc \dfrac x a + \dfrac a {m + 1} \int \dfrac {x^m \rd x} {\sqrt {x^2 - a^2} } & : 0 < \arccsc \dfrac x a < \dfrac \pi 2 \\ \\
\ds \dfrac {x^{m + 1} } {m + 1} \arccsc \dfrac x a - \dfrac a {m + 1} \int \dfrac {x^m \rd x} {\sqrt {x^2 - a^2} } & : -\dfrac \pi 2 < \arccsc \dfrac x a < 0
\end {cases}$</nowiki>

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 Exponential of a x

:$\ds \int e^{a x} \rd x = \frac {e^{a x} } a + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int e^{a x} \cos b x \rd x
      | r = \frac {e^{a x} \cos b x} a + \frac b a \int e^{a x} \sin b x \rd x
      | c = Primitive of $e^{a x} \cos b x$: Lemma
}}
{{eqn | r = \frac {e^{a x} \cos b x} a + \frac b a \paren {\frac {e^{a x} \sin b x} a - \frac b a \int e^{a x} \cos b x \rd x}
      | c = Primitive of $e^{a x} \sin b x$: Lemma
}}
{{eqn | r = \frac {e^{a x} a \cos b x + e^{a x} b \sin b x} {a^2} - \frac {b^2} {a^2} \int e^{a x} \cos b x \rd x
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \paren {1 + \frac {b^2} {a^2} } \int e^{a x} \cos b x \rd x
      | r = \frac {e^{a x} \paren {a \cos b x + b \sin b x} } {a^2} 
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \frac {a^2 + b^2} {a^2} \int e^{a x} \cos b x \rd x
      | r = \frac {e^{a x} \paren {a \cos b x + b \sin b x} } {a^2} 
      | c = common denominator
}}
{{eqn | ll= \leadsto
      | l = \int e^{a x} \cos b x \rd x
      | r = \frac {e^{a x} \paren {a \cos b x + b \sin b x} } {a^2 + b^2} 
      | c = multiplying by $\dfrac {a^2} {a^2 + b^2}$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Exponential of a x

:$\ds \int e^{a x} \rd x = \frac {e^{a x} } a + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int e^{a x} e^{i b x} \rd x
      | r = i \int e^{a x} \sin b x \rd x + \int e^{a x} \cos b x \rd x
      | c = Euler's Formula
}}
{{eqn | ll= \leadsto
      | l = \int e^{a x} \cos b x \rd x
      | r = \map \Re {\int e^{\paren {a + i b} x} \rd x} 
}}
{{eqn | r = \map \Re {\frac {e^{\paren {a + i b} x} } {a + i b} } + C
      | c = Primitive of $e^{a x}$
}}
{{eqn | r = \map \Re {\frac {\paren {a - i b}  e^{\paren {a + i b} x} } {a^2 + b^2} } + C
      | c = multiplying through by $\dfrac {a - i b} {a - i b}$
}}
{{eqn | r = \map \Re {\frac {i a e^{a x} \sin b x + a e^{a x} \cos b x - i b \paren {i e^{a x} \sin b x + e^{a x} \cos b x} } {a^2 + b^2} } + C
      | c = Euler's Formula
}}
{{eqn | r = \map \Re {\frac {i \paren {a e^{a x} \sin b x - b e^{a x} \cos b x} + \paren {a e^{a x} \cos b x + b e^{a x} \sin b x} } { a^2 + b^2} } + C
}}
{{eqn | r = \frac {e^{a x} \paren {a \cos b x + b \sin b x} } {a^2 + b^2} + C
      | c = isolating real part
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Exponential of a x

:$\ds \int e^{a x} \rd x = \frac {e^{a x} } a + C$

Proof:
Let $a, b \in \R_{>0}$ be real constants.
Let $f_1$ and $f_2$ be the real functions defined as:
{{begin-eqn}}
{{eqn | q = \forall x \in \R
      | l = \map {f_1} x
      | r = \map \exp {a x} \map \cos {b x}
}}
{{eqn | l = \map {f_2} x
      | r = \map \exp {a x} \map \sin {b x}
}}
{{end-eqn}}
Let $\map \CC \R$ denote the space of continuous real-valued functions.
Let $\struct {\map {\CC^1} \R, +, \, \cdot \,}_\R$ denote the vector space of continuously differentiable real-valued functions.
Let $S = \span \set {f_1, f_2} \subset \map {\CC^1} \R$ be a vector space.
{{explain|$\span \set {f_1, f_2}$}}
Let $D : S \to S$ be the derivative {{WRT|Differentiation}} $x$.
From Differentiation of Exponential of a x by Cosine of b x and Exponential of a x by Sine of b x wrt x as Nonsingular Matrix, $D$ is expressible as:
:$\mathbf D = \begin {bmatrix} a & b \\ -b & a \end {bmatrix}$
and is nonsingular.
By Inverse of Matrix is Scalar Product of Adjugate by Reciprocal of Determinant:
:$\mathbf D^{-1} = \dfrac 1 {a^2 + b^2} \begin {bmatrix} a & -b \\ b & a \end {bmatrix}$
Then:
{{begin-eqn}}
{{eqn | l = \mathbf D^{-1} \begin {bmatrix} 1 \\ 0 \end {bmatrix}
      | r = \dfrac 1 {a^2 + b^2} \begin {bmatrix} a & -b \\ b & a \end {bmatrix} \begin {bmatrix} 1 \\ 0 \end {bmatrix}
      | c = 
}}
{{eqn | r = \dfrac 1 {a^2 + b^2} \begin {bmatrix} a \\ b \end {bmatrix}
      | c = 
}}
{{end-eqn}}
Application of $\mathbf D$ on both sides on the left and writing out explicitly in terms of $f_1$ and $f_2$ yields:
:$f_1 = \dfrac \d {\d x} \dfrac {a f_1 + b f_2} {a^2 + b^2}$
Integrating {{WRT|Integration}} $x$:
:$\ds \int f_1 \rd x = \frac {a f_1 + b f_2} {a^2 + b^2} + C$
where $C$ is an arbitrary constant.
Substitute definitions of $f_1$ and $f_2$ to get the desired result.
{{qed}}
Theorem: Primitive of Exponential of a x

:$\ds \int e^{a x} \rd x = \frac {e^{a x} } a + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int e^{a x} \sin b x \rd x
      | r = \frac {e^{a x} \sin b x} a - \frac b a \int e^{a x} \cos b x \rd x
      | c = Primitive of $e^{a x} \sin b x$: Lemma
}}
{{eqn | r = \frac {e^{a x} \sin b x} a - \frac b a \paren {\frac {e^{a x} \cos b x} a + \frac b a \int e^{a x} \sin b x \rd x}
      | c = Primitive of $e^{a x} \cos b x$: Lemma
}}
{{eqn | r = \frac {e^{a x} a \sin b x - e^{a x} b \cos b x} {a^2} - \frac {b^2} {a^2} \int e^{a x} \sin b x \rd x
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \paren {1 + \frac {b^2} {a^2} } \int e^{a x} \sin b x \rd x
      | r = \frac {e^{a x} \left({a \sin b x - b \cos b x}\right)} {a^2} 
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \frac {a^2 + b^2} {a^2} \int e^{a x} \sin b x \rd x
      | r = \frac {e^{a x} \paren {a \sin b x - b \cos b x} } {a^2} 
      | c = common denominator
}}
{{eqn | ll= \leadsto
      | l = \int e^{a x} \sin b x \rd x
      | r = \frac {e^{a x} \paren {a \sin b x - b \cos b x} } {a^2 + b^2} 
      | c = multiplying by $\dfrac {a^2} {a^2 + b^2}$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Exponential of a x

:$\ds \int e^{a x} \rd x = \frac {e^{a x} } a + C$

Proof:
{{begin-eqn}}
{{eqn | l = \cos b x + i \sin b x
      | r = e^{i b x}
      | c = Euler's Formula
}}
{{eqn | ll= \leadsto
      | l = e^{a x} \cos b x + i e^{a x} \sin b x
      | r = e^{a x} e^{i b x}
      | c = multiplying both sides by $e^{a x}$
}}
{{eqn | r = e^{\paren {a + i b} x}
      | c = Exponent Combination Laws
}}
{{eqn | ll= \leadsto
      | l = \int e^{a x} \cos b x \, \d x + i \int e^{a x} \sin b x \d x
      | r = \int e^{\paren {a + i b} x} \d x
      | c = Linear Combination of Complex Integrals
}}
{{eqn | r = \frac 1 {a + i b} e^{\paren {a + i b} x} + C
      | c = Primitive of $e^{a x}$
}}
{{eqn | r = \frac {a - i b} {a^2 + b^2} e^{\paren {a + i b} x} + C
      | c = multiplying top and bottom by $a - i b$
}}
{{eqn | r = \frac {a - i b} {a^2 + b^2} e^{a x} e^{i b x} + C
      | c = Exponent Combination Laws
}}
{{eqn | r = \frac {a - i b} {a^2 + b^2} e^{a x} \paren {\cos b x + i \sin b x} + C
      | c = Euler's Formula
}}
{{eqn | r = \frac a {a^2 + b^2} e^{a x} \cos b x - \frac {i b} {a^2 + b^2} e^{a x} \cos b x
}}
{{eqn | o =
      | ro= +
      | r =  \frac {i a} {a^2 + b^2} e^{a x} \sin b x + \frac b {a^2 + b^2} e^{a x} \sin b x + C
}}
{{end-eqn}}
The result follows from equating imaginary parts.
{{qed}}