avewright/proofwiki-math huggingface dataset:
Theorem: Primitive of Cube of Cosine of a x

:$\ds \int \cos^3 a x \rd x = \frac {\sin a x} a - \frac {\sin^3 a x} {3 a} + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \cos^3 a x \rd x
      | r = \int \paren {\frac {3 \cos a x + \cos 3 a x} 4} \rd x
      | c = Power Reduction Formula for $\cos^3$
}}
{{eqn | r = \frac 3 4 \int \cos a x \rd x + \frac 1 4 \int \cos 3 a x \rd x
      | c = Linear Combination of Primitives
}}
{{eqn | r = \frac 3 4 \paren {\frac {\sin a x} a} + \frac 1 4 \paren {\frac {\sin 3 a x} {3 a} } + C
      | c = Primitive of $\cos a x$
}}
{{eqn | r = \frac {3 \sin a x} {4 a} + \frac 1 {12 a} \paren {\sin 3 a x} + C
      | c = simplifying
}}
{{eqn | r = \frac {3 \sin a x} {4 a} + \frac 1 {12 a} \paren {3 \sin a x - 4 \sin^3 a x} + C
      | c = Triple Angle Formula for Sine
}}
{{eqn | r = \frac {3 \sin a x} {4 a} + \frac {\sin a x} {4 a} - \frac {\sin^3 a x} {3 a} + C
      | c = multipying out
}}
{{eqn | r = \frac {\sin a x} a - \frac {\sin^3 a x} {3 a} + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Fourth Power of Cosine of a x

:$\ds \int \cos^4 a x \rd x = \frac {3 x} 8 + \frac {\sin 2 a x} {4 a} + \frac {\sin 4 a x} {32 a} + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \cos^4 a x \rd x
      | r = \int \paren {\frac {3 + 4 \cos 2 x + \cos 4 x} 8} \rd x
      | c = Power Reduction Formula for $\cos^4$
}}
{{eqn | r = \frac 3 8 \int \d x + \frac 1 2 \int \cos 2 a x \rd x + \frac 1 8 \int \cos 4 a x \rd x
      | c = Linear Combination of Primitives
}}
{{eqn | r = \frac {3 x} 8 + \frac 1 2 \int \cos 2 a x \rd x + \frac 1 8 \int \cos 4 a x \rd x + C
      | c = Primitive of Constant
}}
{{eqn | r = \frac {3 x} 8 + \frac 1 2 \paren {\frac {\sin 2 a x} {2 a} } + \frac 1 8 \paren {\frac {\sin 4 a x} {4 a} } + C
      | c = Primitive of $\cos a x$
}}
{{eqn | r = \frac {3 x} 8 + \frac {\sin 2 a x} {4 a} + \frac {\sin 4 a x} {32 a} + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of Square of Cosine of a x

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

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {\cos^2 a x}
      | r = \int \sec^2 a x \rd x
      | c = {{Defof|Cosecant|subdef = Analysis}}
}}
{{eqn | r = \frac {\tan a x} a + C
      | c = Primitive of $\sec^2 a x$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Square of Secant of a x

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

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

:$\ds \int \sec a x \rd x = \frac 1 a \ln \size {\map \tan {\frac \pi 4 + \frac {a x} 2} } + C$
where $\map \tan {\dfrac \pi 4 + \dfrac {a x} 2} \ne 0$.

Proof:
{{begin-eqn}}
{{eqn | l = \int \sec x \rd x
      | r = \ln \size {\map \tan {\frac \pi 4 + \frac x 2} }
      | c = Primitive of $\sec x$: Tangent plus Angle Form
}}
{{eqn | ll= \leadsto
      | l = \int \sec a x \rd x
      | r = \frac 1 a \ln \size {\map \tan {\frac \pi 4 + \frac {a x} 2} } + C
      | c = Primitive of Function of Constant Multiple
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Secant of a x/Secant plus Tangent Form

:$\ds \int \sec a x \rd x = \frac 1 a \ln \size {\sec a x + \tan a x} + C$
where $\sec a x + \tan a x \ne 0$.

Proof:
{{begin-eqn}}
{{eqn | l = \int \sec x \rd x
      | r = \ln \size {\sec x + \tan x}
      | c = Primitive of $\sec x$: Secant plus Tangent Form
}}
{{eqn | ll= \leadsto
      | l = \int \sec a x \rd x
      | r = \frac 1 a \ln \size {\sec a x + \tan a x} + C
      | c = Primitive of Function of Constant Multiple
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power of Secant of a x

:$\ds \int \sec^n a x \rd x = \frac {\sec^{n - 2} a x \tan a x} {a \paren {n - 1} } + \frac {n - 2} {n - 1} \int \sec^{n - 2} a x \rd x$
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 = \sec^{n - 2} a x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = a \paren {n - 2} \sec^{n - 3} a x \sec a x \tan a x
      | c = Derivative of Power, Derivative of $\sec$, Chain Rule for Derivatives
}}
{{eqn | r = a \paren {n - 2} \sec^{n - 2} a x \tan a x
      | c = 
}}
{{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^n a x \rd x
      | r = \int \sec^{n - 2} a x \sec^2 a x \rd x
      | c = 
}}
{{eqn | r = \sec^{n - 2} a x \paren {\frac {\tan a x} a}
      | c = Integration by Parts
}}
{{eqn | o = 
      | ro= -
      | r = \int \paren {\frac {\tan a x} a} \paren {a \paren {n - 2} \sec^{n - 2} a x \tan a x} \rd x
      | c = 
}}
{{eqn | r = \frac {\sec^{n - 2} a x \tan a x} a - \paren {n - 2} \int \tan^2 a x \sec^{n - 2} a x \rd x
      | c = simplifying
}}
{{eqn | r = \frac {\sec^{n - 2} a x \tan a x} a - \paren {n - 2} \int \paren {\sec^2 a x - 1} \sec^{n - 2} a x \rd x
      | c = Difference of $\sec^2$ and $\tan^2$
}}
{{eqn | r = \frac {\sec^{n - 2} a x \tan a x} a - \paren {n - 2} \int \sec^n a x \rd x
      | c = Linear Combination of Primitives
}}
{{eqn | o = 
      | ro= +
      | r = \paren {n - 2} \int \sec^{n - 2} a x \rd x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {n - 1} \int \sec^n a x \rd x
      | r = \frac {\sec^{n - 2} a x \tan a x} a + \paren {n - 2} \int \sec^{n - 2} a x \rd x
      | c = gathering terms
}}
{{eqn | l = \int \sec^n a x \rd x
      | r = \frac {\sec^{n - 2} a x \tan a x} {a \paren {n - 1} } + \frac {n - 2} {n - 1} \int \sec^{n - 2} a x \rd x
      | c = dividing by $n - 1$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of Cube of Cosine of a x

:$\ds \int \frac {\d x} {\cos^3 a x} = \frac {\sin a x} {2 a \cos^2 a x} + \frac 1 {2 a} \ln \size {\map \tan {\frac \pi 4 + \frac {a x} 2} } + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {\cos^3 a x}
      | r = \int \sec^3 a x \rd x
      | c = Secant is Reciprocal of Cosine
}}
{{eqn | 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$
}}
{{eqn | r = \frac {\sin a x} {2 a \cos^2 a x} + \frac 1 2 \int \sec a x \rd x
      | c = Secant is $\dfrac 1 \cos$ and Tangent is $\dfrac \sin \cos$
}}
{{eqn | r = \frac {\sin a x} {2 a \cos^2 a x} + \frac 1 {2 a} \ln \size {\map \tan {\frac \pi 4 + \frac {a x} 2} } + C
      | c = Primitive of $\sec a x$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Cosine of a x by Cosine of b x

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

Proof:
{{begin-eqn}}
{{eqn | l = \int \cos a x \cos b x \rd x
      | r = \int \paren {\frac {\map \cos {a x - b x} + \map \cos {a x + b x} } 2} \rd x
      | c = Werner Formula for Cosine by Cosine
}}
{{eqn | r = \frac 1 2 \int \map \cos {\paren {a - b} x} \rd x + \frac 1 2 \int \map \cos {\paren {a + b} x} \rd x
      | c = Linear Combination of Primitives
}}
{{eqn | r = \frac 1 2 \frac {\map \sin {\paren {a - b} x} } {a - b} + \frac 1 2 \frac {\map \sin {\paren {a + b} x} } {a + b} + C
      | c = Primitive of $\cos a x$
}}
{{eqn | r = \frac {\map \sin {\paren {a - b} x} } {2 \paren {a - b} } + \frac {\map \sin {\paren {a + b} x} } {2 \paren {a + b} } + C
      | c = tidying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of 1 minus Cosine of x/Corollary

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

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {1 - \cos x}
      | r = -\cot \frac x 2 + C
      | c = Primitive of $\dfrac 1 {1 - \cos x}$
}}
{{eqn | ll= \leadsto
      | l = \int \frac {\d x} {1 - \cos a x}
      | r = \frac {-1} a \cot \frac {a x} 2 + C
      | c = Primitive of Function of Constant Multiple
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of x over 1 minus Cosine of a x

:$\ds \int \frac {x \rd x} {1 - \cos a x} = \frac {-x} a \cot \frac {a x} 2 + \frac 2 {a^2} \ln \size {\sin \frac {a 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 = 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 = \frac 1 {1 - \cos a x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {-1} a \cot \frac {a x} 2
      | c = Primitive of $\dfrac 1 {1 - \cos a x}$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \frac {x \rd x} {1 - \cos a x}
      | r = \int u \rd v
      | c = 
}}
{{eqn | r = x \paren {\frac {-1} a \cot \frac {a x} 2} - \int \paren {\frac {-1} a \cot \frac {a x} 2} \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = \frac {-x} a \cot \frac {a x} 2 - \frac {-1} a \paren {\frac 2 a \ln \size {\sin \frac {a x} 2} } + C
      | c = Primitive of $\cot a x$
}}
{{eqn | r = \frac {-x} a \cot \frac {a x} 2 + \frac 2 {a^2} \ln \size {\sin \frac {a x} 2} + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of 1 plus Cosine of x/Corollary

:$\ds \int \frac {\d x} {1 + \cos a x} = \frac 1 a \tan \frac {a x} 2 + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {1 + \cos x}
      | r = \tan \frac x 2 + C
      | c = Primitive of $\dfrac 1 {1 + \cos x}$
}}
{{eqn | ll= \leadsto
      | l = \int \frac {\d x} {1 + \cos a x}
      | r = \frac 1 a \tan \frac {a x} 2 + C
      | c = Primitive of Function of Constant Multiple
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of x over 1 plus Cosine of a x

:$\ds \int \frac {x \rd x} {1 + \cos a x} = \frac x a \tan \frac {a x} 2 + \frac 2 {a^2} \ln \size {\cos \frac {a 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 = 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 = \frac 1 {1 + \cos a x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac 1 a \tan \frac {a x} 2
      | c = Primitive of $\dfrac 1 {1 + \cos a x}$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \frac {x \rd x} {1 + \cos a x}
      | r = \int u \rd v
      | c = 
}}
{{eqn | r = x \paren {\frac 1 a \tan \frac {a x} 2} - \int \paren {\frac 1 a \tan \frac {a x} 2} \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = \frac x a \tan \frac {a x} 2 - \frac 1 a \paren {\frac {-2} a \ln \size {\cos a x} } + C
      | c = Primitive of $\tan a x$
}}
{{eqn | r = \frac x a \tan \frac {a x} 2 + \frac 2 {a^2} \ln \size {\cos \frac {a x} 2} + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of Square of 1 minus Cosine of a x

:$\ds \int \frac {\d x} {\paren {1 - \cos a x}^2} = \frac {-1} {2 a} \cot \frac {a x} 2 - \frac 1 {6 a} \cot^3 \frac {a x} 2 + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {\paren {1 - \cos a x}^2}
      | r = \int \paren {\frac 1 2 \csc^2 \frac {a x} 2}^2 \rd x
      | c = Reciprocal of One Minus Cosine
}}
{{eqn | r = \frac 1 4 \int \csc^4 \frac {a x} 2 \rd x
      | c = simplifying
}}
{{eqn | r = \frac 1 4 \paren {\frac{-\csc^2 \dfrac {a x} 2 \cot \dfrac {a x} 2} {\dfrac {3 a} 2} + \frac 2 3 \int \csc^2 \frac {a x} 2 \rd x} + C
      | c = Primitive of $\csc^n a x$
}}
{{eqn | r = \frac {-1} {6 a} \csc^2 \frac {a x} 2 \cot \dfrac {a x} 2 + \frac 1 6 \int \csc^2 \frac {a x} 2 \rd x + C
      | c = simplifying
}}
{{eqn | r = \frac {-1} {6 a} \csc^2 \frac {a x} 2 \cot \dfrac {a x} 2 + \frac 1 6 \paren {\frac {-2} a \cot \frac {a x} 2} + C
      | c = Primitive of $\csc^2 a x$
}}
{{eqn | r = \frac {-1} {6 a} \paren {1 + \cot^2 \frac {a x} 2} \cot \dfrac {a x} 2 - \frac 2 {6 a} \cot \frac {a x} 2 + C
      | c = Difference of Squares of Cosecant and Cotangent
}}
{{eqn | r = \frac {-1} {2 a} \cot \frac {a x} 2 - \frac 1 {6 a} \cot^3 \frac {a x} 2 + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of Square of 1 plus Cosine of a x

:$\ds \int \frac {\d x} {\paren {1 + \cos a x}^2} = \frac 1 {2 a} \tan \frac {a x} 2 + \frac 1 {6 a} \tan^3 \frac {a x} 2 + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {\paren {1 + \cos a x}^2}
      | r = \int \paren {\frac 1 2 \sec^2 \frac {a x} 2}^2 \rd x
      | c = Reciprocal of One Plus Cosine
}}
{{eqn | r = \frac 1 4 \int \sec^4 \frac {a x} 2 \rd x
      | c = simplifying
}}
{{eqn | r = \frac 1 4 \paren {\frac {\sec^2 \dfrac {a x} 2 \tan \dfrac {a x} 2} {\dfrac {3 a} 2} + \frac 2 3 \int \sec^2 \frac {a x} 2 \rd x} + C
      | c = Primitive of $\sec^n a x$
}}
{{eqn | r = \frac 1 {6 a} \sec^2 \frac {a x} 2 \tan \dfrac {a x} 2 + \frac 1 6 \int \sec^2 \frac {a x} 2 \rd x + C
      | c = simplifying
}}
{{eqn | r = \frac 1 {6 a} \sec^2 \frac {a x} 2 \tan \dfrac {a x} 2 + \frac 1 6 \paren {\frac 2 a \tan \frac {a x} 2} + C
      | c = Primitive of $\sec^2 a x$
}}
{{eqn | r = \frac 1 {6 a} \paren {1 + \tan^2 \frac {a x} 2} \tan \dfrac {a x} 2 + \frac 2 {6 a} \tan \frac {a x} 2 + C
      | c = Difference of Squares of Secant and Tangent
}}
{{eqn | r = \frac 1 {2 a} \tan \frac {a x} 2 + \frac 1 {6 a} \tan^3 \frac {a x} 2 + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of p plus q by Cosine of a x

:<nowiki>$\ds \int \frac {\rd x} {p + q \cos a x} = \begin {cases} 
\dfrac 2 {a \sqrt {p^2 - q^2} } \map \arctan {\sqrt {\dfrac {p - q} {p + q} } \tan \dfrac {a x} 2} + C & : p^2 > q^2 \\ \\
\dfrac 1 {a \sqrt {q^2 - p^2} } \ln \size {\dfrac {\tan \dfrac {a x} 2 + \sqrt {\dfrac {q + p} {q - p} } } {\tan \dfrac {a x} 2 - \sqrt {\dfrac {q + p} {q - p} } } } + C & : p^2 < q^2 \\
\end {cases}$</nowiki>
for $p \ne q$.

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {p + q \cos a x}
      | r = \frac 2 {a \paren {p - q} } \int \frac {\d u} {u^2 + \dfrac {p + q} {p - q} }
      | c = Weierstrass Substitution: $u = \tan \dfrac {a x} 2$
}}
{{end-eqn}}
Let $p^2 > q^2$.
Then, by Sign of Quotient of Factors of Difference of Squares:
:$\dfrac {p + q} {p - q} > 0$
Thus, let $\dfrac {p + q} {p - q} = d^2$.
Then:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {p + q \cos a x}
      | r = \frac 2 {a \paren {p - q} } \int \frac {\d u} {u^2 + d^2}
      | c = 
}}
{{eqn | r = \frac 2 {a \paren {p - q} } \frac 1 d \arctan \frac u d + C
      | c = Primitive of $\dfrac 1 {x^2 + a^2}$
}}
{{eqn | r = \frac 2 {a \paren {p - q} } \frac 1 {\sqrt {\dfrac {p + q} {p - q} } } \map \arctan {\frac {\tan \dfrac {a x} 2} {\sqrt {\dfrac {p + q} {p - q} } } } + C
      | c = substituting for $u$ and $d$
}}
{{eqn | r = \frac 2 {a \sqrt {p^2 - q^2} } \map \arctan {\sqrt {\frac {p - q} {p + q} } \tan \dfrac {a x} 2} + C
      | c = simplifying
}}
{{end-eqn}}
{{qed|lemma}}
Now let $p^2 < q^2$.
Then, by Sign of Quotient of Factors of Difference of Squares:
:$\dfrac {p + q} {p - q} < 0$
Thus, let:
:$-\dfrac {p + q} {p - q} = d^2$
or:
:$\dfrac {q + p} {q - p} = d^2$
Then:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {p + q \cos a x}
      | r = \frac 2 {a \paren {p - q} } \int \frac {\d u} {u^2 - d^2}
      | c = 
}}
{{eqn | r = \frac 2 {a \paren {p - q} } \frac 1 {2 d} \ln \size {\frac {u - d} {u + d} } + C
      | c = Primitive of $\dfrac 1 {x^2 - a^2}$
}}
{{eqn | r = \frac 1 {a \paren {p - q} } \frac 1 {\sqrt {\dfrac {q + p} {q - p} } } \ln \size {\frac {\tan \dfrac {a x} 2 - \sqrt {\dfrac {q + p} {q - p} } } {\tan \dfrac {a x} 2 + \sqrt {\dfrac {q + p} {q - p} } } } + C
      | c = substituting for $u$ and $d$
}}
{{eqn | r = \frac 1 {a \sqrt {q^2 - p^2} } \ln \size {\frac {\tan \dfrac {a x} 2 - \sqrt {\dfrac {q + p} {q - p} } } {\tan \dfrac {a x} 2 + \sqrt {\dfrac {q + p} {q - p} } } } + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of square of p plus q by Cosine of a x

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

Proof:
{{begin-eqn}}
{{eqn | l = \map {\dfrac \d {\d x} } {\dfrac {\sin a x} {p + q \cos a x} }
      | r = \dfrac {\paren {p + q \cos a x} \map {\frac \d {\d x} } {\sin a x} - \sin a x \map {\frac \d {\d x} } {p + q \sin a x} } {\paren {p + q \cos a x}^2}
      | c = Quotient Rule for Derivatives
}}
{{eqn | r = \dfrac {\paren {p + q \cos a x} \paren {a \cos a x} - \sin a x \paren {-a q \sin a x} } {\paren {p + q \cos a x}^2}
      | c = Derivative of Cosine Function, Derivative of Sine Function
}}
{{eqn | r = a \dfrac {p \cos a x + q \paren {\cos^2 a x + \sin^2 a x} } {\paren {p + q \cos a x}^2}
      | c = simplification
}}
{{eqn | r = a \dfrac {p \cos a x + q} {\paren {p + q \cos a x}^2}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = a \dfrac {p q \cos a x + q^2} {q \paren {p + q \cos a x}^2}
      | c = 
}}
{{eqn | r = a \dfrac {p q \cos a x + q^2 + p^2 - p^2} {q \paren {p + q \cos a x}^2}
      | c = 
}}
{{eqn | r = a \dfrac {q^2 - p^2} {q \paren {p + q \cos a x}^2} + a \dfrac {p q \cos a x + p^2} {q \paren {p + q \cos a x}^2}
      | c = 
}}
{{eqn | r = a \dfrac {q^2 - p^2} {q \paren {p + q \cos a x}^2} + a \dfrac {p \paren {p + q \cos a x} } {q \paren {p + q \cos a x}^2}
      | c = 
}}
{{eqn | r = \dfrac {a \paren {q^2 - p^2} } {q \paren {p + q \cos a x}^2} + \dfrac {a p} q \dfrac 1 {p + q \cos a x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac q {a \paren {q^2 - p^2} } \map {\dfrac \d {\d x} } {\dfrac {\sin a x} {p + q \cos a x} }
      | r = \dfrac 1 {\paren {p + q \cos a x}^2} + \dfrac p {\paren {q^2 - p^2} } \dfrac 1 {p + q \cos a x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac q {a \paren {q^2 - p^2} } {\dfrac {\sin a x} {p + q \cos a x} }
      | r = \int \dfrac {\d x} {\paren {p + q \cos a x}^2} + \dfrac p {\paren {q^2 - p^2} } \int \dfrac {\d x} {p + q \cos a x}
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Primitive of Reciprocal of p squared plus square of q by Cosine of a x

:$\ds \int \frac {\d x} {p^2 + q^2 \cos^2 a x} = \frac 1 {a p \sqrt{p^2 + q^2} } \arctan \frac {p \tan a x} {\sqrt {p^2 + q^2} } + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {p^2 + q^2 \cos^2 a x}
      | r = \int \frac {\csc^2 a x \rd x} {p^2 \csc^2 a x + q^2 \cot^2 a x}
      | c = multiplying the numerator and the denominator by $\csc^2 a x$
}}
{{eqn | r = \int \frac {\csc^2 a x \rd x} {p^2 + \paren {p^2 + q^2} \cot^2 a x}
      | c = Difference of Squares of Cosecant and Cotangent
}}
{{eqn | r = \int \frac {-\paren {\cot a x}' \rd x} {a p^2 + a \paren {p^2 + q^2} \cot^2 a x}
      | c = Derivative of Cotangent Function
}}
{{eqn | r = \int \frac {-\d t} {a p^2 + a \paren {p^2 + q^2} t^2}
      | c = putting $t = \cot a x$
}}
{{eqn | r = \frac {-1} {a \paren {p^2 + q^2} } \int \frac {\d t} {\paren {\tfrac p {\sqrt {p^2 + q^2} } }^2 + t^2}
      | c = 
}}
{{eqn | r = \frac {-1} {a \paren {p^2 + q^2} } \frac {\sqrt {p^2 + q^2} } p \, \map \arctan {\frac {\sqrt {p^2 + q^2} } p t } + C
      | c = Primitive of $\dfrac 1 {x^2 + a^2}$
}}
{{eqn | r = \frac {-1} {a p \sqrt {p^2 + q^2} } \map \arctan {\frac {\sqrt {p^2 + q^2} } p t} + C
      | c = 
}}
{{eqn | r = \frac {-1} {a p \sqrt {p^2 + q^2} } \map \arctan {\frac {\sqrt {p^2 + q^2} } p \cot a x} + C
      | c = substituting $t = \cot a x$
}}
{{eqn | r = \frac {-1} {a p \sqrt {p^2 + q^2} } \map \arctan {\frac {\sqrt {p^2 + q^2} } {p \tan a x} } + C
      | c = 
}}
{{eqn | r = \frac {-1} {a p \sqrt {p^2 + q^2} } \map \arccot {\frac {p \tan a x} {\sqrt {p^2 + q^2} } } + C
      | c = Arctangent of Reciprocal equals Arccotangent
}}
{{eqn | r = \frac 1 {a p \sqrt {p^2 + q^2} } \paren {\map \arctan {\frac {p \tan a x} {\sqrt {p^2 + q^2} } } - \frac \pi 2} + C
      | c = Sum of Arctangent and Arccotangent
}}
{{eqn | r = \frac 1 {a p \sqrt {p^2 + q^2} } \map \arctan {\frac {p \tan a x} {\sqrt {p^2 + q^2} } } + C
      | c = absorbing into the arbitrary constant
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power of x by Cosine of a x

:$\ds \int x^m \cos a x \rd x = \frac {x^m \sin a x} a + \frac {m x^{m - 1} \cos a x} {a^2} - \frac {m \paren {m - 1} } {a^2} \int x^{m - 2} \cos a x \rd x$

Proof:
=== Lemma ===
{{:Primitive of Power of x by Cosine of a x/Lemma}}{{qed|lemma}}
From {{Lemma|Primitive of Power of x by Sine of a x|proof = yes|disp = Primitive of $x^{m - 1} \sin a x$}}:
:$(1): \quad \ds \int x^{m - 1} \sin a x \rd x = \frac {-x^{m - 1} \cos a x} a + \frac {m - 1} a \int x^{m - 2} \cos a x \rd x$
So:
{{begin-eqn}}
{{eqn | l = \int x^m \cos a x \rd x
      | r = \frac {x^m \sin a x} a - \frac m a \int x^{m - 1} \sin a x \rd x
      | c = {{Lemma|Primitive of Power of x by Cosine of a x}}
}}
{{eqn | r = \frac {x^m \sin a x} a - \frac m a \paren {\frac {-x^{m - 1} \cos a x} a + \frac {m - 1} a \int x^{m - 2} \cos a x \rd x}
      | c = from $(1)$
}}
{{eqn | r = \frac {x^m \sin a x} a + \frac {m x^{m - 1} \cos a x} {a^2} - \frac {m \paren {m - 1} } {a^2} \int x^{m - 2} \cos a x \rd x
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Cosine of a x over Power of x

:$\ds \int \frac {\cos a x} {x^n} \rd x = \frac {-\cos a x} {\paren {n - 1} x^{n - 1} } - \frac a {n - 1} \int \frac {\sin a x} {x^{n - 1} } \rd x$

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