avewright/proofwiki-math huggingface dataset:
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:
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 Exponential of a x by Cosine of b x

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

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

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

:$\ds \int x e^{a x} \sin b x \rd x = \frac {x e^{a x} \paren {a \sin b x - b \cos b x} } {a^2 + b^2} - \frac {e^{a x} \paren {\paren {a^2 - b^2} \sin b x - 2 a b \cos b x} } {\paren {a^2 + b^2}^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
      | 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} \sin b x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {e^{a x} \paren {a \sin b x - b \cos b x} } {a^2 + b^2}
      | c = Primitive of $e^{a x} \sin b x$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int x e^{a x} \sin b x \rd x
      | r = x \paren {\frac {e^{a x} \paren {a \sin b x - b \cos b x} } {a^2 + b^2} } - \int \paren {\frac {e^{a x} \paren {a \sin b x - b \cos b x} } {a^2 + b^2} } \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = \frac {x e^{a x} \paren {a \sin b x - b \cos b x} } {a^2 + b^2}
      | c = Linear Combination of Primitives
}}
{{eqn | o = 
      | ro= -
      | r = \frac a {a^2 + b^2} \int e^{a x} \sin b x \rd x + \frac b {a^2 + b^2} \int e^{a x} \cos b x \rd x + C
      | c = 
}}
{{eqn | r = \frac {x e^{a x} \paren {a \sin b x - b \cos b x} } {a^2 + b^2}
      | c = 
}}
{{eqn | o = 
      | ro= -
      | r = \frac a {a^2 + b^2} \paren {\frac {e^{a x} \paren {a \sin b x - b \cos b x} } {a^2 + b^2} }
      | c = Primitive of $e^{a x} \sin b x$
}}
{{eqn | o = 
      | ro= +
      | r = \frac b {a^2 + b^2} \paren {\frac {e^{a x} \paren {a \cos b x + b \sin b x} } {a^2 + b^2} } + C
      | c = Primitive of $e^{a x} \cos b x$
}}
{{eqn | r = \frac {x e^{a x} \paren {a \sin b x - b \cos b x} } {a^2 + b^2} - \frac {e^{a x} \paren {\paren {a^2 - b^2} \sin b x - 2 a b \cos b x} } {\paren {a^2 + b^2}^2} + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of x by Exponential of a x by Cosine of b x

:$\ds \int x e^{a x} \cos b x \rd x = \frac {x e^{a x} \paren {a \cos b x + b \sin b x} } {a^2 + b^2} - \frac {e^{a x} \paren {\paren {a^2 - b^2} \cos b x - 2 a b \sin b x} } {\paren {a^2 + b^2}^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
      | 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} \cos b x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {e^{a x} \paren {a \cos b x + b \sin b x} } {a^2 + b^2}
      | c = Primitive of $e^{a x} \cos b x$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int x e^{a x} \sin b x \rd x
      | r = x \paren {\frac {e^{a x} \paren {a \cos b x + b \sin b x} } {a^2 + b^2} } - \int \paren {\frac {e^{a x} \paren {a \cos b x + b \sin b x} } {a^2 + b^2} } \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = \frac {x e^{a x} \paren {a \cos b x + b \sin b x} } {a^2 + b^2}
      | c = Linear Combination of Primitives
}}
{{eqn | o = 
      | ro= -
      | r = \frac a {a^2 + b^2} \int e^{a x} \cos b x \rd x - \frac b {a^2 + b^2} \int e^{a x} \sin b x \rd x + C
      | c = 
}}
{{eqn | r = \frac {x e^{a x} \paren {a \cos b x + b \sin b x} } {a^2 + b^2}
      | c = 
}}
{{eqn | o = 
      | ro= -
      | r = \frac a {a^2 + b^2} \paren {\frac {e^{a x} \paren {a \cos b x + b \sin b x} } {a^2 + b^2} }
      | c = Primitive of $e^{a x} \cos b x$
}}
{{eqn | o = 
      | ro= -
      | r = \frac b {a^2 + b^2} \paren {\frac {e^{a x} \paren {a \sin b x - b \cos b x} } {a^2 + b^2} } + C
      | c = Primitive of $e^{a x} \sin b x$
}}
{{eqn | r = \frac {x e^{a x} \paren {a \cos b x + b \sin b x} } {a^2 + b^2} - \frac {e^{a x} \paren {\paren {a^2 - b^2} \cos b x - 2 a b \sin b x} } {\paren {a^2 + b^2}^2} + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Exponential of a x by Logarithm of x

:$\ds \int e^{a x} \ln x \rd x = \frac {e^{a x} \ln x} a - \frac 1 a \int \frac {e^{a x} } x \rd 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 = \ln x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = \frac 1 x
      | c = Derivative of Natural Logarithm
}}
{{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 e^{a x} \ln x \rd x
      | r = \ln x \paren {\frac {e^{a x} } a} - \int \paren {\frac {e^{a x} } a} \frac 1 x \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = \frac {e^{a x} \ln x} a - \frac 1 a \int \frac {e^{a x} } x \rd x + C
      | c = Primitive of Constant Multiple of Function
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Logarithm of x

:$\ds \int \ln x \rd x = x \ln x - 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 = \ln x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = \frac 1 x
      | c = Derivative of $\ln x$
}}
{{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 \ln x \rd x
      | r = x \ln x - \int x \paren {\frac 1 x} \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = x \ln x - \int \rd x + C
      | c = simplifying
}}
{{eqn | r = x \ln x - x + C
      | c = Primitive of Constant
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Logarithm of x

:$\ds \int \ln x \rd x = x \ln x - x + C$

Proof:
Note that we have: 
{{begin-eqn}}
{{eqn	| l = \int_0^1 \ln x \rd x
	| r = \int_0^1 x^0 \paren {\ln x}^1 \rd x
}}
{{eqn	| r = \frac {\paren {-1}^1 \map \Gamma 2} {1^2}
	| c = Definite Integral from $0$ to $1$ of $x^m \paren {\ln x}^n$
}}
{{eqn	| r = -1
	| c = Gamma Function Extends Factorial
}}
{{end-eqn}}
We therefore have: 
{{begin-eqn}}
{{eqn	| l = -1
	| r = \int_0^1 \ln x \rd x
}}
{{eqn	| r = \frac 1 a \int_0^a \map \ln {\frac u a} \rd u
	| c = substituting $x = \dfrac u a$ where $a > 0$
}}
{{eqn	| r = \frac 1 a \int_0^a \paren {\ln u - \ln a} \rd u
	| c = Difference of Logarithms
}}
{{eqn	| r = \frac 1 a \int_0^a \ln u \rd u - \ln a
	| c = Primitive of Constant, Fundamental Theorem of Calculus
}}
{{end-eqn}}
giving: 
:$\ds \frac 1 a \int_0^a \ln u \rd u = \ln a - 1$
so: 
:$\ds \int_0^a \ln u \rd u = a \ln a - a$
for all real $a > 0$. 
By Fundamental Theorem of Calculus: First Part, we have that: 
:$x \ln x - x$ is a primitive of $\ln x$ on $x > 0$.
We therefore conclude that, by Primitives which Differ by Constant:
:$\ds \int \ln x \rd x = x \ln x - x + C$
for $x > 0$.
{{qed}}
Theorem: Primitive of x by Logarithm of x

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

Proof:
{{begin-eqn}}
{{eqn | l = \int x \map \ln {x^2 + a^2} \rd x
      | r = \frac {x^2 \map \ln {x^2 + a^2} } 2 - \int \frac {x^3} {x^2 + a^2} \rd x + C
      | c = Primitive of $x^m \map \ln {x^2 + a^2}$ with $m = 1$
}}
{{eqn | r = \frac {x^2 \map \ln {x^2 + a^2} } 2 - \paren {\frac {x^2} 2 - \frac {a^2} 2 \map \ln {x^2 + a^2} } + C
      | c = Primitive of $\dfrac {x^3} {x^2 + a^2}$
}}
{{eqn | r = \frac {\paren {x^2 + a^2} \map \ln {x^2 + a^2} - x^2} 2 + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of x by Logarithm of x

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

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

Proof:
From Primitive of $x^m \ln x$:
:$\ds \int x^m \ln x \rd x = \frac {x^{m + 1} } {m + 1} \paren {\ln x - \frac 1 {m + 1} } + C$
The result follows by setting $m = 1$.
{{qed}}
Theorem: Primitive of Power of x by Logarithm of x

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

:$\ds \int \frac {\ln x} x \rd x = \frac {\ln^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 = \ln x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = \frac 1 x
      | c = Derivative of $\ln x$
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = \frac 1 x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \ln x
      | c = Primitive of Reciprocal
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \frac {\ln x} x \rd x
      | r = \ln x \ln x - \int \ln x \paren {\frac 1 x} \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = \ln^2 x - \int \frac {\ln x} x \rd x + C
      | c = tidying
}}
{{eqn | ll= \leadsto
      | l = 2 \int \frac {\ln x} x \rd x
      | r = \ln^2 x + C
      | c = adding $\ds\int \frac {\ln x} x \rd x$ to both sides
}}
{{eqn | ll= \leadsto
      | l = \int \frac {\ln x} x \rd x
      | r = \frac {\ln^2 x} 2 + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Logarithm of x over x squared

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

Proof:
From Primitive of $x^m \ln x$:
:$\ds \int x^m \ln x \rd x = \frac {x^{m + 1} } {m + 1} \paren {\ln x - \frac 1 {m + 1} } + C$
Thus:
{{begin-eqn}}
{{eqn | l = \int \frac {\ln x} {x^2} \rd x
      | r = \frac {x^{-1} } {-1} \paren {\ln x - \frac 1 {-1} } + C
      | c = Primitive of $x^m \ln x$, setting $m = -2$
}}
{{eqn | r = \frac {-\ln x} x - \frac 1 x + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Square of Logarithm of x

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

:$\ds \int \frac {\ln^n x} x \rd x = \frac {\ln^{n + 1} x} {n + 1} + C$

Proof:
{{begin-eqn}}
{{eqn | l = z
      | r = \ln x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d z} {\d x}
      | r = \frac 1 x
      | c = Derivative of Natural Logarithm
}}
{{eqn | ll= \leadsto
      | l = \int \frac {\ln^n x} x \rd x
      | r = \int z^n \rd z
      | c = Integration by Substitution
}}
{{eqn | r = \frac {z^{n + 1} } {n + 1} + C
      | c = Primitive of Power
}}
{{eqn | r = \frac {\ln^{n + 1} x} {n + 1} + C
      | c = substituting for $z$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of x by Logarithm of x

:$\ds \int \frac {\d x} {x \ln x} = \ln \size {\ln x} + C$

Proof:
{{begin-eqn}}
{{eqn | l = z
      | r = \ln x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d z} {\d x}
      | r = \frac 1 x
      | c = Derivative of Natural Logarithm
}}
{{eqn | ll= \leadsto
      | l = \int \frac {\d x} {x \ln x}
      | r = \ln \size {\ln x} + C
      | c = Primitive of Function under its Derivative
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of Logarithm of x

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

Proof:
From Primitive of $\dfrac {x^m} {\ln x}$:
:$\ds \int \frac {x^m \rd x} {\ln x} = \map \ln {\ln x} + \paren {m + 1} \ln x + \sum_{k \mathop \ge 2}^n \frac {\paren {m + 1}^k \paren {\ln x}^k} {k \times k!} + C$
The result follows by setting $m = 0$.
{{qed}}
Theorem: Primitive of Power of x over Logarithm of x

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

Proof:
{{begin-eqn}}
{{eqn | l = u
      | r = \ln x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = e^u
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \d x
      | r = e^u \d u
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \int \frac {x^m \rd x} {\ln x}
      | r = \int \frac {\paren {e^u}^m e^u \rd u} u
      | c = 
}}
{{eqn | r = \int \frac {e^{u \paren {m + 1} } \rd u} u
      | c = 
}}
{{eqn | r = \ln u + \sum_{k \mathop \ge 1} \frac {\paren {\paren {m + 1} u}^k} {k \times k!} + C
      | c = Primitive of $\dfrac {e^{a x} } x$: $u > 0$ for $x > 1$
}}
{{eqn | r = \map \ln {\ln x} + \sum_{k \mathop \ge 1} \frac {\paren {m + 1}^k \paren {\ln x}^k} {k \times k!} + C
      | c = substituting $u = \ln x$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power of Logarithm of x

:$\ds \int \ln^n x \rd x = x \ln^n x - n \int \ln^{n - 1} x \rd 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 = \ln^n x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = n \ln^{n - 1} x \frac 1 x
      | c = Derivative of $\ln x$, Derivative of Power, Chain Rule for Derivatives
}}
{{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 \ln^n x \rd x
      | r = x \ln^n x - \int x \paren {n \ln^{n - 1} x \frac 1 x} \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = x \ln^n x - n \int \ln^{n - 1} x \rd x + C
      | c = Primitive of Constant Multiple of Function
}}
{{end-eqn}}
{{qed}}