avewright/proofwiki-math huggingface dataset:
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 = \int e^{a x} \paren {\frac {e^{i b x} - e^{-i b x} } {2 i} } \rd x
      | c = Euler's Sine Identity
}}
{{eqn | r = \frac 1 {2 i} \int e^{a x} \paren {e^{i b x} - e^{-i b x} } \rd x
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \frac 1 {2 i} \int \paren {e^{a x} e^{i b x} - e^{a x} e^{-i b x} } \rd x
      | c = 
}}
{{eqn | r = \frac 1 {2 i} \int \paren {e^{a x + i b x} - e^{a x - i b x} } \rd x
      | c = Product of Powers
}}
{{eqn | r = \frac 1 {2 i} \int e^{a x + i b x} \rd x - \frac 1 {2 i} \int e^{a x - i b x} \rd x
      | c = Linear Combination of Primitives
}}
{{eqn | r = \frac 1 {2 i} \int e^{\paren {a + i b} x} \rd x - \frac 1 {2 i} \int e^{\paren {a - i b} x} \rd x
      | c = 
}}
{{eqn | r = \frac 1 {2 i} \frac {e^{\paren {a + i b} x} } {a + i b} - \frac 1 {2 i} \frac {e^{\paren {a - i b} x} } {a - i b} + C
      | c = Primitive of $e^{a x}$
}}
{{eqn | r = \frac 1 {2 i} \frac {e^{a x + i b x} } {a + i b} - \frac 1 {2 i} \frac {e^{a x - i b x} } {a - i b} + C
      | c = 
}}
{{eqn | r = \frac 1 {2 i} \frac {e^{a x} e^{i b x} } {a + i b} - \frac 1 {2 i} \frac {e^{a x} e^{-i b x} } {a - i b} + C
      | c = Product of Powers
}}
{{eqn | r = \frac 1 {2 i} \frac {e^{a x} e^{i b x} \paren {a - i b} } {\paren {a + i b} \paren {a - i b} } - \frac 1 {2 i} \frac {e^{a x} e^{-i b x} \paren {a + i b} } {\paren {a - i b} \paren {a + i b} } + C
      | c = 
}}
{{eqn | r = \frac {e^{a x} e^{i b x} \paren {a - i b} - e^{a x} e^{-i b x} \paren {a + i b} } {2 i \paren {a + i b} \paren {a - i b} } + C
      | c = 
}}
{{eqn | r = \frac {e^{a x} e^{i b x} \paren {a - i b} - e^{a x} e^{-i b x} \paren {a + i b} } {2 i \paren {a^2 + b^2} } + C
      | c = Product of Complex Number with Conjugate
}}
{{eqn | r = \frac {a e^{a x} e^{i b x} - i b e^{a x} e^{i b x} - a e^{a x} e^{-i b x} - i b e^{a x} e^{-i b x} } {2 i \paren {a^2 + b^2} } + C
      | c = 
}}
{{eqn | r = \frac {e^{a x} } {\paren {a^2 + b^2} } \paren {\frac {a e^{i b x} - i b e^{i b x} - a e^{-i b x} - i b e^{-i b x} } {2 i} } + C
      | c = 
}}
{{eqn | r = \frac {e^{a x} } {\paren {a^2 + b^2} } \paren {a \frac {e^{i b x} - e^{-i b x} } {2 i} - b \frac {e^{i b x} + e^{-i b x} } 2} + C
      | c = 
}}
{{eqn | r = \frac {e^{a x} } {\paren {a^2 + b^2} } \paren {a \frac {e^{i b x} - e^{-i b x} } {2 i} - b \cos b x} + C
      | c = Euler's Cosine Identity
}}
{{eqn | r = \frac {e^{a x} } {\paren {a^2 + b^2} } \paren {a \sin b x - b \cos b x} + C
      | c = Euler's Sine Identity
}}
{{eqn | r = \frac {e^{a x} \paren {a \sin b x - b \cos b x} } {a^2 + b^2} + C
      | c = 
}}
{{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, x \in \R$ be real numbers.
Suppose $a \ne 0 \ne b$.
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$ be the space of continuous real-valued functions.
Let $\struct {\map {\CC^1} \R, +, \, \cdot \,}_\R$ be 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.
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} 0 \\ 1 \end {bmatrix}
      | r = \dfrac 1 {a^2 + b^2} \begin {bmatrix} a & -b \\ b & a \end {bmatrix} \begin {bmatrix} 0 \\ 1 \end {bmatrix}
      | c = 
}}
{{eqn | r = \dfrac 1 {a^2 + b^2} \begin {bmatrix} -b \\ a \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_2 = \ds \dfrac \d {\d x} \frac {-b f_1 + a f_2} {a^2 + b^2}$
Integrate {{WRT|Integration}} $x$:
:$\ds \int f_2 \rd x = \frac {-b f_1 + a 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 x by Exponential of a x

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

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

Let $n$ be a positive integer.
Let $a$ be a non-zero real number.
Then:
{{begin-eqn}}
{{eqn | l = \int x^n e^{a x} \rd x
      | r = \frac {e^{a x} } a \paren {x^n - \dfrac {n x^{n - 1} } a + \dfrac {n \paren {n - 1} x^{n - 2} } {a^2} - \dfrac {n \paren {n - 1} \paren {n - 2} x^{n - 3} } {a^3} + \cdots + \dfrac {\paren {-1}^n n!} {a^n} } + C
      | c = 
}}
{{eqn | r = \frac {e^{a x} } a \sum_{k \mathop = 0}^n \paren {\paren {-1}^k \frac {n^{\underline k} x^{n - k} } {a^k} } + C
      | c = 
}}
{{end-eqn}}
where $n^{\underline k}$ denotes the $k$th falling factorial power of $n$.

Proof:
Proof by induction:
For all $n \in \N_{> 0}$, let $\map P n$ be the proposition:
:$\ds \int x^n e^{a x} \rd x = \frac {e^{a x} } a \sum_{k \mathop = 0}^n \paren {\paren {-1}^k \frac {n^{\underline k} x^{n - k} } {a^k} } + C$
$\map P 0$ is true, as from Primitive of $e^{a x}$:
:$\ds \int e^{a x} \rd x = \frac {e^{a x} } a$
Theorem: Primitive of Exponential of a x over x

For $x > 0$:
{{begin-eqn}}
{{eqn | l = \int \frac {e^{a x} \rd x} x
      | r = \ln x + \sum_{k \mathop \ge 1} \frac {\paren {a x}^k} {k \times k!} + C
      | c = 
}}
{{eqn | r = \ln x + \dfrac {a x} {1 \times 1!} + \dfrac {\paren {a x}^2} {2 \times 2!} + \dfrac {\paren {a x}^3} {3 \times 3!} + \cdots + C
      | c = 
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {e^{a x} \rd x} x
      | r = \int \frac 1 x \paren {\sum_{k \mathop = 0}^\infty \frac {\paren {a x}^k} {k!} } \rd x
      | c = Power Series Expansion for Exponential Function
}}
{{eqn | r = \int \frac 1 x \paren {1 + \sum_{k \mathop = 1}^\infty \frac {\paren {a x}^k} {k!} } \rd x
      | c = extracting the case $k = 0$ from the expansion
}}
{{eqn | n = 1
      | r = \int \frac {\d x} x + \sum_{k \mathop = 1}^\infty \frac {a^k} {k!} \int x^{k - 1} \rd x
      | c = Linear Combination of Primitives
}}
{{eqn | r = \ln x + \sum_{k \mathop = 1}^\infty \frac {a^k} {k!} \int x^{k - 1} \rd x
      | c = Primitive of Reciprocal: $x > 0$ so negative argument does not apply
}}
{{eqn | r = \ln x + \sum_{k \mathop = 1}^\infty \frac {a^k} {k!} \frac {x^k} k + C
      | c = Primitive of Power
}}
{{eqn | r = \ln x + \sum_{k \mathop \ge 1} \frac {\paren {a x}^k} {k \times k!} + C
      | c = simplification
}}
{{end-eqn}}
The validity of $(1)$ follows from absolute convergence of the power series expansion.
{{qed}}
Theorem: Primitive of Exponential of a x over Power of x

:$\ds \int \frac {e^{a x} \rd x} {x^n} = \frac {-e^{a x} } {\paren {n - 1} x^{n - 1} } + \frac a {n - 1} \int \frac {e^{a x} \rd x} {x^{n - 1} } + C$
where $n \ne 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 = e^{a x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = a e^{a x}
      | c = Derivative of $e^{a x}$
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = \frac 1 {x^n}
      | c = 
}}
{{eqn | r = x^{-n}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {x^{-n + 1} } {-n + 1}
      | c = Primitive of Power
}}
{{eqn | r = \frac {-1} {\paren {n - 1} x^{n - 1} }
      | c = simplifying
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \frac {e^{a x} \rd x} {x^n}
      | r = e^{a x} \paren {\frac {-1} {\paren {n - 1} x^{n - 1} } } - \int \paren {\frac {-1} {\paren {n - 1} x^{n - 1} } } \paren {a e^{a x} } \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = \frac {-e^{a x} } {\paren {n - 1} x^{n - 1} } + \frac a {n - 1} \int \frac {e^{a x} \rd x} {x^{n - 1} } + C
      | c = Primitive of Constant Multiple of Function
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of p plus q by Exponential of a x

:$\ds \int \frac {\d x} {p + q e^{a x} } = \frac x p - \frac 1 {a p} \ln \size {p + q e^{a x} } + C$

Proof:
{{begin-eqn}}
{{eqn | l = z
      | r = p + q e^{a x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d z} {\d x}
      | r = a q e^{a x}
      | c = Derivative of $e^{a x}$
}}
{{eqn | r = a \paren {z - p}
      | c = in terms of $z$
}}
{{eqn | ll= \leadsto
      | l = \int \frac {\d x} {p + q e^{a x} }
      | r = \int \frac {\d z} {a \paren {z - p} z}
      | c = Integration by Substitution
}}
{{eqn | r = \frac 1 a \int \frac {\d z} {z \paren {z - p} }
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \frac 1 a \paren {\frac 1 {-p} \ln \size {\frac z {z - p} } } + C
      | c = Primitive of $\dfrac 1 {x \paren {a x + b} }$
}}
{{eqn | r = \frac {-1} {a p} \ln \size {\frac {p + q e^{a x} } {q e^{a x} } } + C
      | c = substituting for $z$
}}
{{eqn | r = \frac {-1} {a p} \paren {\ln \size {p + q e^{a x} } - \ln \size {q e^{a x} } } + C
      | c = Difference of Logarithms
}}
{{eqn | r = \frac {-1} {a p} \paren {\ln \size {p + q e^{a x} } - \paren {\ln \size {e^{a x} } + \ln \size q} } + C
      | c = Sum of Logarithms
}}
{{eqn | r = \frac {-1} {a p} \ln \size {p + q e^{a x} } + \frac 1 {a p} \map \ln {e^{a x} } + \frac 1 {a p} \ln \size q + C
      | c = $e^{a x}$ always positive
}}
{{eqn | r = \frac {-1} {a p} \ln \size {p + q e^{a x} } + \frac 1 {a p} \map \ln {e^{a x} } + C
      | c = $\dfrac 1 {a p} \ln \size q$ subsumed into arbitrary constant
}}
{{eqn | r = \frac {-1} {a p} \ln \size {p + q e^{a x} } + \frac 1 {a p} a x + C
      | c = Exponential of Natural Logarithm
}}
{{eqn | r = \frac x p - \frac 1 {a p} \ln \size {p + q e^{a x} } + C
      | c = simplification
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of Square of p plus q by Exponential of a x

:$\ds \int \frac {\d x} {\paren {p + q e^{a x} }^2} = \frac x {p^2} + \frac 1 {a p \paren {p + q e^{a x} } } - \frac 1 {a p^2} \ln \size {p + q e^{a x} } + C$

Proof:
{{begin-eqn}}
{{eqn | l = z
      | r = p + q e^{a x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d z} {\d x}
      | r = a q e^{a x}
      | c = Derivative of $e^{a x}$
}}
{{eqn | r = a \paren {z - p}
      | c = in terms of $z$
}}
{{eqn | ll= \leadsto
      | l = \int \frac {\d x} {p + q e^{a x} }
      | r = \int \frac {\d z} {a \paren {z - p} z^2}
      | c = Integration by Substitution
}}
{{eqn | r = \frac 1 a \int \frac {\d z} {z^2 \paren {z - p} }
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \frac 1 a \paren {\frac {-1} {-p z} + \frac 1 {\paren {-p}^2} \ln \size {\frac {z - p} z} } + C
      | c = Primitive of $\dfrac 1 {x^2 \paren {a x + b} }$
}}
{{eqn | r = \frac 1 {a p z} + \frac 1 {a p^2} \ln \size {\frac {z - p} z} + C
      | c = simplifying
}}
{{eqn | r = \frac 1 {a p \paren {p + q e^{a x} } } + \frac 1 {a p^2} \ln \size {\frac {q e^{a x} } {p + q e^{a x} } } + C
      | c = substituting for $z$
}}
{{eqn | r = \frac 1 {a p \paren {p + q e^{a x} } } + \frac 1 {a p^2} \ln \size {q e^{a x} } - \frac 1 {a p^2} \ln \size {p + q e^{a x} } + C
      | c = Difference of Logarithms
}}
{{eqn | r = \frac 1 {a p \paren {p + q e^{a x} } } + \frac 1 {a p^2} \ln \size q + \frac 1 {a p^2} \ln \size {e^{a x} } - \frac 1 {a p^2} \ln \size {p + q e^{a x} } + C
      | c = Sum of Logarithms
}}
{{eqn | r = \frac 1 {a p \paren {p + q e^{a x} } } + \frac 1 {a p^2} \ln \size q + \frac 1 {a p^2} \map \ln {e^{a x} } - \frac 1 {a p^2} \ln \size {p + q e^{a x} } + C
      | c = $e^{a x}$ always positive
}}
{{eqn | r = \frac 1 {a p \paren {p + q e^{a x} } } + \frac 1 {a p^2} \map \ln {e^{a x} } - \frac 1 {a p^2} \ln \size {p + q e^{a x} } + C
      | c = $\dfrac 1 {a p^2} \ln \size q$ subsumed into constant
}}
{{eqn | r = \frac 1 {a p \paren {p + q e^{a x} } } + \frac 1 {a p^2} a x - \frac 1 {a p^2} \ln \size {p + q e^{a x} } + C
      | c = Exponential of Natural Logarithm
}}
{{eqn | r = \frac x {p^2} + \frac 1 {a p \paren {p + q e^{a x} } } - \frac 1 {a p^2} \ln \size {p + q e^{a x} } + C
      | c = simplification
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of p by Exponential of a x plus q by Exponential of -a x

:$\ds \int \frac {\d x} {p e^{a x} + q e^{-a x} } = \begin{cases}
\dfrac 1 {a \sqrt {p q} } \map \arctan {\sqrt {\dfrac p q} e^{a x} } & : \sqrt {p q} > 0 \\
\dfrac 1 {2 a \sqrt {-p q} } \ln \size {\dfrac {e^{a x} - \sqrt {-\dfrac q p} } {e^{a x} + \sqrt {-\dfrac q p} } } & : \sqrt {p q} < 0 \\
\end{cases}$

Proof:
{{begin-eqn}}
{{eqn | l = z
      | r = e^{a x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d z} {\d x}
      | r = a e^{a x}
      | c = Derivative of $e^{a x}$
}}
{{eqn | ll= \leadsto
      | l = \int \frac {\d x} {p e^{a x} + q e^{-a x} }
      | r = \int \frac 1 {p z + q z^{-1} } \frac {\d z} {a z}
      | c = Integration by Substitution
}}
{{eqn | r = \frac 1 {a p} \int \frac {\d z} {z^2 + \dfrac q p}
      | c = Primitive of Constant Multiple of Function
}}
{{end-eqn}}
Let $\dfrac q p > 0$.
Then:
{{begin-eqn}}
{{eqn | l = \frac 1 {a p} \int \frac {\d z} {z^2 + \dfrac q p}
      | r = \frac 1 {a p} \paren {\frac 1 {\sqrt {q / p} } \arctan \frac z {\sqrt {q / p} } } + C
      | c = Primitive of $\dfrac 1 {x^2 + a^2}$
}}
{{eqn | r = \frac 1 {a \sqrt {p q} } \map \arctan {\sqrt {\frac p q} z}
      | c = simplifying
}}
{{eqn | r = \frac 1 {a \sqrt {p q} } \map \arctan {\sqrt {\frac p q} e^{a x} }
      | c = substituting for $z$
}}
{{end-eqn}}
Let $\dfrac q p < 0$.
Then let $d^2 = -\dfrac q p$ and so:
{{begin-eqn}}
{{eqn | l = \frac 1 {a p} \int \frac {\d z} {z^2 + \dfrac q p}
      | r = \frac 1 {a p} \int \frac {\d z} {z^2 - d^2}
      | c = 
}}
{{eqn | r = \frac 1 {a p} \paren {\frac 1 {2 d} \ln \size {\frac {z - d} {z + d} } } + C
      | c = Primitive of $\dfrac 1 {x^2 - a^2}$
}}
{{eqn | r = \frac 1 {a p} \paren {\frac 1 {2 \sqrt {-q / p} } \ln \size {\frac {z - \sqrt {-q / p} } {z + \sqrt {-q / p} } } } + C
      | c = substituting for $d$
}}
{{eqn | r = \frac 1 {2 a \sqrt {-p q} } \ln \size {\frac {z - \sqrt {-\frac q p} } {z + \sqrt {-\frac q p} } } + C
      | c = simplifying
}}
{{eqn | r = \frac 1 {2 a \sqrt {-p q} } \ln \size {\frac {e^{a x} - \sqrt {-\frac q p} } {e^{a x} + \sqrt {-\frac q p} } } + C
      | c = substituting for $z$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Exponential of a x by Sine of b x

:$\ds \int e^{a x} \sin b x \rd x = \frac {e^{a x} \paren {a \sin b x - b \cos b x} } {a^2 + b^2} + 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 by Sine of b x

:$\ds \int e^{a x} \sin b x \rd x = \frac {e^{a x} \paren {a \sin b x - b \cos b x} } {a^2 + b^2} + 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}}
Theorem: Primitive of Exponential of a x by Sine of b x

:$\ds \int e^{a x} \sin b x \rd x = \frac {e^{a x} \paren {a \sin b x - b \cos b x} } {a^2 + b^2} + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int e^{a x} \sin b x \rd x
      | r = \int e^{a x} \paren {\frac {e^{i b x} - e^{-i b x} } {2 i} } \rd x
      | c = Euler's Sine Identity
}}
{{eqn | r = \frac 1 {2 i} \int e^{a x} \paren {e^{i b x} - e^{-i b x} } \rd x
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \frac 1 {2 i} \int \paren {e^{a x} e^{i b x} - e^{a x} e^{-i b x} } \rd x
      | c = 
}}
{{eqn | r = \frac 1 {2 i} \int \paren {e^{a x + i b x} - e^{a x - i b x} } \rd x
      | c = Product of Powers
}}
{{eqn | r = \frac 1 {2 i} \int e^{a x + i b x} \rd x - \frac 1 {2 i} \int e^{a x - i b x} \rd x
      | c = Linear Combination of Primitives
}}
{{eqn | r = \frac 1 {2 i} \int e^{\paren {a + i b} x} \rd x - \frac 1 {2 i} \int e^{\paren {a - i b} x} \rd x
      | c = 
}}
{{eqn | r = \frac 1 {2 i} \frac {e^{\paren {a + i b} x} } {a + i b} - \frac 1 {2 i} \frac {e^{\paren {a - i b} x} } {a - i b} + C
      | c = Primitive of $e^{a x}$
}}
{{eqn | r = \frac 1 {2 i} \frac {e^{a x + i b x} } {a + i b} - \frac 1 {2 i} \frac {e^{a x - i b x} } {a - i b} + C
      | c = 
}}
{{eqn | r = \frac 1 {2 i} \frac {e^{a x} e^{i b x} } {a + i b} - \frac 1 {2 i} \frac {e^{a x} e^{-i b x} } {a - i b} + C
      | c = Product of Powers
}}
{{eqn | r = \frac 1 {2 i} \frac {e^{a x} e^{i b x} \paren {a - i b} } {\paren {a + i b} \paren {a - i b} } - \frac 1 {2 i} \frac {e^{a x} e^{-i b x} \paren {a + i b} } {\paren {a - i b} \paren {a + i b} } + C
      | c = 
}}
{{eqn | r = \frac {e^{a x} e^{i b x} \paren {a - i b} - e^{a x} e^{-i b x} \paren {a + i b} } {2 i \paren {a + i b} \paren {a - i b} } + C
      | c = 
}}
{{eqn | r = \frac {e^{a x} e^{i b x} \paren {a - i b} - e^{a x} e^{-i b x} \paren {a + i b} } {2 i \paren {a^2 + b^2} } + C
      | c = Product of Complex Number with Conjugate
}}
{{eqn | r = \frac {a e^{a x} e^{i b x} - i b e^{a x} e^{i b x} - a e^{a x} e^{-i b x} - i b e^{a x} e^{-i b x} } {2 i \paren {a^2 + b^2} } + C
      | c = 
}}
{{eqn | r = \frac {e^{a x} } {\paren {a^2 + b^2} } \paren {\frac {a e^{i b x} - i b e^{i b x} - a e^{-i b x} - i b e^{-i b x} } {2 i} } + C
      | c = 
}}
{{eqn | r = \frac {e^{a x} } {\paren {a^2 + b^2} } \paren {a \frac {e^{i b x} - e^{-i b x} } {2 i} - b \frac {e^{i b x} + e^{-i b x} } 2} + C
      | c = 
}}
{{eqn | r = \frac {e^{a x} } {\paren {a^2 + b^2} } \paren {a \frac {e^{i b x} - e^{-i b x} } {2 i} - b \cos b x} + C
      | c = Euler's Cosine Identity
}}
{{eqn | r = \frac {e^{a x} } {\paren {a^2 + b^2} } \paren {a \sin b x - b \cos b x} + C
      | c = Euler's Sine Identity
}}
{{eqn | r = \frac {e^{a x} \paren {a \sin b x - b \cos b x} } {a^2 + b^2} + C
      | c = 
}}
{{end-eqn}}
{{qed}}