avewright/proofwiki-math huggingface dataset:
Theorem: Primitive of x by Tangent of a x

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

Proof:
From Power Series Expansion for Tangent Function:
{{:Power Series Expansion for Tangent Function}}
{{begin-eqn}}
{{eqn | l = x \tan ax
      | r = \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n - 1} 2^{2 n} \paren {2^{2 n} - 1} B_{2 n} a^{2 n - 1} x^{2 n} } {\paren {2 n}!}
      | c =
}}
{{eqn | ll= \leadsto
      | l = \int x \tan a x \rd x
      | r = \int \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n - 1} 2^{2 n} \paren {2^{2 n} - 1} B_{2 n} a^{2 n - 1} x^{2 n} } {\paren {2 n}!} \rd x
      | c =
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty \paren {\int \frac {\paren{-1}^{n - 1} 2^{2 n} \paren {2^{2 n} - 1} B_{2 n} a^{2 n - 1} x^{2 n} } {\paren {2 n}!} \rd x}
      | c =
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty \paren {\frac {\paren {-1}^{n - 1} 2^{2 n} \paren {2^{2 n} - 1} B_{2 n} a^{2 n - 1} } {\paren {2 n}!} \times \int x^{2 n} \rd x}
      | c =
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty \paren {\frac {\paren {-1}^{n - 1} 2^{2 n} \paren {2^{2 n} - 1} B_{2 n} a^{2 n - 1} } {\paren {2 n}!} \times \frac {x^{2 n + 1} } {2 n + 1} + C}
      | c = Primitive of Power
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n - 1} 2^{2 n} \paren {2^{2 n} - 1} B_{2 n} a^{2 n - 1} x^{2 n + 1} } {\paren {2 n + 1}!} + C
      | c =
}}
{{eqn | ll= \leadsto
      | l = \int x \tan a x \rd x
      | r = \frac 1 {a ^ 2} \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n - 1} 2^{2 n} \paren {2^{2 n} - 1} B_{2 n} \paren {a x}^{2 n + 1} } {\paren {2 n + 1}!} + C
      | c =
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Tangent of a x over x

:$\ds \int \frac {\tan a x} x \rd x = a x + \frac {\paren {a x}^3} 9 + \frac {2 \paren {a x}^5} {75} + \cdots + \frac {\paren {-1}^{n - 1} 2^{2 n} \paren {2^{2 n} - 1} B_{2 n} \paren {a x}^{2 n - 1} } {\paren {2 n - 1} \paren {2 n}!} + \cdots + C$
where $B_n$ denotes the $n$th Bernoulli number.

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

:$\ds \int x \tan^2 a x \rd x = \frac {x \tan a x} a + \frac 1 {a^2} \ln \size {\cos a x} - \frac {x^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 = Primitive of Power
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = \tan^2 a x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {\tan a x} a - x
      | c = Primitive of $\tan^2 a x$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int x \tan^2 a x \rd x
      | r = x \paren {\frac {\tan a x} a - x} - \int \paren {\frac {\tan a x} a - x} \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = \frac {x \tan a x} a - x^2 - \int \paren {\frac {\tan a x} a - x} \rd x + C
      | c = simplifying
}}
{{eqn | r = \frac {x \tan a x} a - x^2 - \frac 1 a \int \tan a x \rd x + \int x \rd x + C
      | c = Linear Combination of Primitives
}}
{{eqn | r = \frac {x \tan a x} a - x^2 - \frac 1 a \paren {\frac {-\ln \size {\cos a x} } a} + \int x \rd x + C
      | c = Primitive of $\tan a x$
}}
{{eqn | r = \frac {x \tan a x} a - x^2 + \frac 1 {a^2} \ln \size {\cos a x} + \frac {x^2} 2 + C
      | c = Primitive of Power
}}
{{eqn | r = \frac {x \tan a x} a + \frac 1 {a^2} \ln \size {\cos a x} - \frac {x^2} 2 + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of p plus q by Tangent of a x

:$\ds \int \frac {\d x} {p + q \tan a x} = \frac {p x} {p^2 + q^2} + \frac q {a \paren {p^2 + q^2} } \ln \size {q \sin a x + p \cos a x} + C$

Proof:
First, let $\arctan \dfrac p q = \phi$.
Let $z = a x + \phi$.
{{begin-eqn}}
{{eqn | l = z
      | r = \map \sin {a x + \phi}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d z} {\d x}
      | r = a \map \cos {a x + \phi}
      | c = Derivative of $\sin a x$ etc.
}}
{{eqn | r = a \cos z
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {p + q \tan a x}
      | r = \int \frac {\d x} {p + q \dfrac {\sin a x} {\cos a x} }
      | c = Tangent is Sine divided by Cosine
}}
{{eqn | r = \int \frac {\cos a x \rd x} {p \cos a x + q \sin a x}
      | c = multiplying top and bottom by $\cos a x$
}}
{{eqn | r = \int \frac {\cos a x \rd x} {\sqrt {p^2 + q^2} \map \sin {a x + \phi} }
      | c = Multiple of Sine plus Multiple of Cosine: Sine Form
}}
{{eqn | r = \frac 1 {\sqrt {p^2 + q^2} } \int \frac {\cos a x \rd x} {\map \sin {a x + \phi} }
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \frac 1 {\sqrt {p^2 + q^2} } \paren {\frac {\ln \size {\map \sin {a x + \phi} } } {a \cos \phi} + \tan \phi \int \frac {\sin a x \rd x} {\map \sin {a x + \phi} } + C}
      | c = Primitive of $\dfrac {\cos a x} {\map \sin {a x + \phi} }$
}}
{{end-eqn}}
{{finish}}
Theorem: Primitive of Reciprocal of p plus q by Tangent of a x

:$\ds \int \frac {\d x} {p + q \tan a x} = \frac {p x} {p^2 + q^2} + \frac q {a \paren {p^2 + q^2} } \ln \size {q \sin a x + p \cos a x} + C$

Proof:
We have:
:$\dfrac \d {\d x} \paren {q \sin a x + p \cos a x} = a q \cos a x - a p \sin a x$
Thus:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {p + q \tan a x}
      | r = \int \frac {\d x} {p + q \dfrac {\sin a x} {\cos a x} }
      | c = Tangent is Sine divided by Cosine
}}
{{eqn | r = \int \frac {\cos a x \rd x} {p \cos a x + q \sin a x}
      | c = 
}}
{{eqn | r = \frac 1 {p^2 + q^2} \int \frac {\paren {p^2 + q^2} \cos a x \rd x} {p \cos a x + q \sin a x}
      | c = 
}}
{{eqn | r = \frac 1 {p^2 + q^2} \int \frac {p^2 \cos a x + p q \sin a x - p q \sin a x + q^2 \cos a x} {p \cos a x + q \sin a x} \rd x
      | c = 
}}
{{eqn | r = \frac 1 {p^2 + q^2} \paren {\int \frac {p^2 \cos a x + p q \sin a x} {p \cos a x + q \sin a x} \rd x + \int \frac {-p q \sin a x + q^2 \cos a x} {p \cos a x + q \sin a x} \rd x}
      | c = 
}}
{{eqn | r = \frac 1 {p^2 + q^2} \paren {\int p \rd x + \frac q a \int \frac {\map \d {p \cos a x + q \sin a x} } {p \cos a x + q \sin a x} }
      | c = 
}}
{{eqn | r = \frac {p x} {p^2 + q^2} + \frac q {a \paren {p^2 + q^2} } \ln \size {p \cos a x + q \sin a x} + C
      | c = Primitive of Constant and Primitive of Reciprocal
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power of Tangent of a x

:$\ds \int \tan^n a x \rd x = \frac {\tan^{n - 1} a x} {\paren {n - 1} a} - \int \tan^{n - 2} a x \rd x$
for $n \ne 1$.

Proof:
{{begin-eqn}}
{{eqn | l = \int \tan^n a x \rd x
      | r = \int \tan^{n - 2} a x \tan^2 a x \rd x
      | c = 
}}
{{eqn | r = \int \tan^{n - 2} a x \paren {\sec^2 a x - 1} \rd x
      | c = Difference of Squares of Secant and Tangent
}}
{{eqn | r = \int \tan^{n - 2} a x \sec^2 a x \rd x - \int \tan^{n - 2} \rd x
      | c = Linear Combination of Primitives
}}
{{eqn | r = \frac {\tan^{n - 1} a x} {\paren {n - 1} a} - \int \tan^{n - 2} \rd x
      | c = Primitive of $\tan^n a x \sec^2 a x$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Square of Cotangent of a x

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

Proof:
{{begin-eqn}}
{{eqn | l = \int \cot^2 x \rd x
      | r = -\cot x - x
      | c = Primitive of $\cot^2 x$
}}
{{eqn | ll= \leadsto
      | l = \int \cot a x \rd x
      | r = \frac 1 a \paren {-\cot a x - a x} + C
      | c = Primitive of Function of Constant Multiple
}}
{{eqn | r = \frac {-\cot a x} a - x + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Cube of Cotangent of a x

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

Proof:
{{begin-eqn}}
{{eqn | l = \int \cot^3 x \rd x
      | r = \int \cot a x \cot^2 a x \rd x
      | c = 
}}
{{eqn | r = \int \cot a x \paren {\csc^2 a x - 1} \rd x
      | c = Difference of Squares of Cosecant and Cotangent
}}
{{eqn | r = \int \cot a x \csc^2 a x \rd x - \int \cot a x \rd x
      | c = Linear Combination of Primitives
}}
{{eqn | r = \frac {-\cot^2 a x} {2 a} - \int \cot a x \rd x + C
      | c = Primitive of $\cot^n a x \csc^2 a x$: $n = 1$
}}
{{eqn | r = \frac {-\cot^2 a x} {2 a} - \paren {\frac {\ln \size {\sin a x} } a} + C
      | c = Primitive of $\cot a x$
}}
{{eqn | r = \frac {-\cot^2 a x} {2 a} - \frac 1 a \ln \size {\sin a x} + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power of Cotangent of a x by Square of Cosecant of a x

:$\ds \int \cot^n a x \csc^2 a x \rd x = \frac {-\cot^{n + 1} a x} {\paren {n + 1} a} + C$

Proof:
{{begin-eqn}}
{{eqn | l = z
      | r = \cot a x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d z} {\d x}
      | r = -a \csc^2 a x
      | c = Derivative of $\cot a x$
}}
{{eqn | ll= \leadsto
      | l = \int \cot^n a x \csc^2 a x \rd x
      | r = \int \frac {-1} a z^n \rd z
      | c = Integration by Substitution
}}
{{eqn | r = \frac {-1} a \frac {z^{n + 1} } {n + 1}
      | c = Primitive of Power
}}
{{eqn | r = \frac {-\cot^{n + 1} a x} {\paren {n + 1} a} + C
      | c = substituting for $z$ and simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Square of Cosecant of a x over Cotangent of a x

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

Proof:
{{begin-eqn}}
{{eqn | l = \frac \d {\d x} \cot x
      | r = -\csc^2 x
      | c = Derivative of Cotangent Function
}}
{{eqn | ll= \leadsto
      | l = \int \frac {\csc^2 x \rd x} {\cot x}
      | r = -\ln \size {\cot a x} + C
      | c = Primitive of Function under its Derivative
}}
{{eqn | ll= \leadsto
      | l = \int \frac {\csc^2 a x \rd x} {\cot a x}
      | r = \frac 1 a \paren {-\ln \size {\cot a x} } + C
      | c = Primitive of Function of Constant Multiple
}}
{{eqn | r = \frac {-\ln \size {\cot a x} } a + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of Cotangent of a x

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

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {\cot a x}
      | r = \int \tan a x \rd x
      | c = Cotangent is Reciprocal of Tangent
}}
{{eqn | r = \frac {-\ln \size {\cos a x} } a + C
      | c = Primitive of $\tan a x$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of x by Cotangent of a x

:$\ds \int x \cot a x \rd x = \frac 1 {a ^ 2} \paren {a x - \frac {\paren {a x}^3} 9 - \frac {\paren {a x}^5} {225} - \cdots + \frac {\paren {-1}^n 2^{2 n} B_{2 n} \paren {a x}^{2 n + 1} } {\paren {2 n + 1} !} + \cdots} + C$
where $B_{2 n}$ denotes the $2 n$th Bernoulli number.

Proof:
From Power Series Expansion for Cotangent Function:
{{:Power Series Expansion for Cotangent Function}}
{{begin-eqn}}
{{eqn | l = x \cot ax
      | r = \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^n 2^{2 n} B_{2 n} a^{2 n - 1} x^{2 n} } {\paren {2 n}!}
      | c =
}}
{{eqn | ll= \leadsto
      | l = \int x \cot a x \rd x
      | r = \int \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^n 2^{2 n} B_{2 n} a^{2 n - 1} x^{2 n} } {\paren {2 n}!} \rd x
      | c =
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \paren {\int \frac {\paren {-1}^n 2^{2 n} B_{2 n} a^{2 n - 1} x^{2 n} } {\paren {2 n}!} \rd x}
      | c =
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \paren {\frac {\paren {-1}^n 2^{2 n} B_{2 n} a^{2 n - 1} } {\paren {2 n}!} \times \int x^{2 n} \rd x}
      | c =
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \paren {\frac {\paren {-1}^n 2^{2 n} B_{2 n} a^{2 n - 1} } {\paren {2 n}!} \times \frac {x^{2 n + 1} } {2 n + 1} + C}
      | c = Primitive of Power
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^n 2^{2 n} B_{2 n} a^{2 n - 1} x^{2 n + 1} } {\paren {2 n + 1}!} + C
      | c =
}}
{{eqn | ll= \leadsto
      | l = \int x \cot a x \rd x
      | r = \frac 1 {a^2} \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^n 2^{2 n} B_{2 n} \paren {a x}^{2 n + 1} } {\paren {2 n + 1}!} + C
      | c =
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Cotangent of a x over x

:$\ds \int \frac {\cot a x} x \rd x = \frac {-1} a x - \frac {a x} 3 - \frac {\paren {a x}^3} {135} - \cdots - \frac {\paren {-1}^{n - 1} 2^{2 n} B_{2 n} \paren {a x}^{2 n - 1} } {\paren {2 n - 1} \paren {2 n}!} - \cdots + C$
where $B_n$ denotes the $n$th Bernoulli number.

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

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

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

Proof:
We have:
:$\dfrac \d {\d x} \paren {p \sin a x + q \cos a x} = a p \cos a x - a q \sin a x$
Thus:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {p + q \cot a x}
      | r = \int \frac {\d x} {p + q \dfrac {\cos a x} {\sin a x} }
      | c = Cotangent is Cosine divided by Sine
}}
{{eqn | r = \int \frac {\sin a x \rd x} {p \sin a x + q \cos a x}
      | c = 
}}
{{eqn | r = \frac 1 {p^2 + q^2} \int \frac {\paren {p^2 + q^2} \sin a x \rd x} {p \sin a x + q \cos a x}
      | c = 
}}
{{eqn | r = \frac 1 {p^2 + q^2} \int \frac {p^2 \sin a x + p q \cos a x - p q \cos a x + q^2 \sin a x} {p \sin a x + q \cos a x} \rd x
      | c = 
}}
{{eqn | r = \frac 1 {p^2 + q^2} \paren {\int \frac {p^2 \sin a x + p q \cos a x} {p \sin a x + q \cos a x} \rd x + \int \frac {-p q \cos a x + q^2 \sin a x} {p \sin a x + q \cos a x} \rd x}
      | c = 
}}
{{eqn | r = \frac 1 {p^2 + q^2} \paren {\int p \rd x - \frac q a \int \frac {\map \d {p \sin a x + q \cos a x} } {p \sin a x + q \cos a x} }
      | c = 
}}
{{eqn | r = \frac {p x} {p^2 + q^2} - \frac q {a \paren {p^2 + q^2} } \ln \size {p \sin a x + q \cos a x} + C
      | c = Primitive of Constant and Primitive of Reciprocal
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power of Cotangent of a x

:$\ds \int \cot^n a x \rd x = \frac {-\cot^{n - 1} a x} {\paren {n - 1} a} - \int \cot^{n - 2} a x \rd x$
for $n \ne 1$.

Proof:
{{begin-eqn}}
{{eqn | l = \int \cot^n a x \rd x
      | r = \int \cot^{n - 2} a x \cot^2 a x \rd x
      | c = 
}}
{{eqn | r = \int \cot^{n - 2} a x \paren {\csc^2 a x - 1} \rd x
      | c = Difference of Squares of Cosecant and Cotangent
}}
{{eqn | r = \int \cot^{n - 2} a x \csc^2 a x \rd x - \int \cot^{n - 2} \rd x
      | c = Linear Combination of Primitives
}}
{{eqn | r = \frac {-\cot^{n - 1} a x} {\paren {n - 1} a} - \int \cot^{n - 2} \rd x
      | c = Primitive of $\cot^n a x \csc^2 a x$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Cube of Secant of a x

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

Proof:
{{begin-eqn}}
{{eqn | l = \int \sec^3 x \rd x
      | r = \frac {\sec a x \tan a x} {2 a} + \frac 1 2 \int \sec a x \rd x
      | c = Primitive of $\sec^n a x$ where $n = 3$
}}
{{eqn | r = \frac {\sec a x \tan a x} {2 a} + \frac 1 2 \paren {\frac 1 a \ln \size {\sec a x + \tan a x} }
      | c = Primitive of $\sec a x$
}}
{{eqn | r = \frac 1 {2 a} \paren {\sec a x \tan a x + \ln \size {\sec a x + \tan a x} } + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Cube of Secant of a x

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

Proof:
With a view to expressing the primitive in the form:
:$\ds \int u \frac {\d v} {\d x} \rd x = u v - \int v \frac {\d u} {\d x} \rd x$
let:
{{begin-eqn}}
{{eqn | l = u
      | r = \sec a x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = a \sec a x \tan a x
      | c = Derivative of Function of Constant Multiple, Derivative of $\sec$
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = \sec^2 a x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {\tan a x} a
      | c = Primitive of $\sec^2 a x$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \sec^3 a x \rd x
      | r = \int \sec a x \sec^2 a x \rd x
      | c = 
}}
{{eqn | r = \sec a x \frac {\tan a x} a - \int \paren {\frac {\tan a x} a} \paren {a \sec a x \tan a x} \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = \frac 1 a \sec a x \tan a x - \int \tan^2 a x \sec a x \rd x + C
      | c = simplifying
}}
{{eqn | r = \frac 1 a \sec a x \tan a x - \int \paren {\sec^2 a x - 1} \sec a x \rd x + C
      | c = Difference of $\sec^2$ and $\tan^2$
}}
{{eqn | r = \frac 1 a \sec a x \tan a x - \int \sec^3 a x \rd x + \int \sec a x \rd x + C
      | c = Linear Combination of Primitives
}}
{{eqn | ll= \leadsto
      | l = 2 \int \sec^3 a x \rd x
      | r = \frac 1 a \sec a x \tan a x + \int \sec a x \rd x + C
      | c = simplifying
}}
{{eqn | r = \frac 1 a \sec a x \tan a x + \frac 1 a \ln \size {\sec a x + \tan a x} + C
      | c = Primitive of $\sec a x$
}}
{{end-eqn}}
The result follows.
{{qed}}
Theorem: Primitive of Reciprocal of Secant of a x

:$\ds \int \frac {\d x} {\sec a x} = \frac {\sin a x} a + C$

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

{{begin-eqn}}
{{eqn | l = \int x \sec a x \rd x
      | r = \frac 1 {a^2} \paren {\frac {\paren {a x}^2} 2 - \frac {\paren {a x}^4} 8 + \frac {5 \paren {a x}^6} {144} - \cdots + \frac {\paren {-1}^n E_{2 n} \paren {a x}^{2 n + 2} } {\paren {2 n + 2} \paren {2 n}!} + \cdots} + C
      | c = 
}}
{{eqn | r = \frac 1 {a^2} \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^n E_{2 n} \paren {a x}^{2 n + 2} } {\paren {2 n + 2} \paren {2 n}!} + C
      | c = 
}}
{{end-eqn}}
where $E_{2 n}$ is the $2 n$th Euler number.

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

:$\ds \int \frac {\sec a x} x \rd x = \ln \size x + \frac {\paren {a x}^2} 4 + \frac {5 \paren {a x}^4} {96} + \frac {61 \paren {a x}^6} {4320} + \cdots + \frac {\paren {-1}^n E_n \paren {a x}^{2 n} } {\paren {2 n} \paren {2 n}!} + \cdots + C$
where $E_n$ is the $n$th Euler number.

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

:$\ds \int x \sec^2 a x \rd x = \frac {x \tan a x} a + \frac  1 {a^2} \ln \size {\cos a x} + C$

Proof:
With a view to expressing the primitive in the form:
:$\ds \int u \frac {\d v} {\d x} \rd x = u v - \int v \frac {\d u} {\d x} \rd x$
let:
{{begin-eqn}}
{{eqn | l = u
      | r = x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = 1
      | c = Derivative of Identity Function
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = \sec^2 a x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {\tan a x} a
      | c = Primitive of $\sec^2 a x$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int x \sec^2 a x \rd x
      | r = \frac {x \tan a x} a - \int \frac {\tan a x} a \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = \frac {x \tan a x} a - \frac 1 a \paren {\frac {-1} a \ln \size {\cos a x} } + C
      | c = Primitive of $\tan a x$
}}
{{eqn | r = \frac {x \tan a x} a + \frac  1 {a^2} \ln \size {\cos a x} + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}