avewright/proofwiki-math huggingface dataset:
Theorem: One Plus Tangent Half Angle over One Minus Tangent Half Angle

:$\dfrac {1 + \tan \frac x 2} {1 - \tan \frac x 2} = \sec x + \tan x$

Proof:
{{begin-eqn}}
{{eqn | l = \frac {1 + \tan \frac x 2}{1 - \tan \frac x 2}
      | r = \frac {1 + \frac {\sin \frac x 2}{\cos \frac x 2} }{1 - \frac {\sin \frac x 2}{\cos \frac x 2} }
      | c = Tangent is Sine divided by Cosine
}}
{{eqn | r = \frac {\cos \frac x 2 + \sin \frac x 2}{\cos \frac x 2 - \sin \frac x 2}
      | c = multiply top and bottom by $\cos \dfrac x 2$
}}
{{eqn | r = \frac {\cos \frac x 2 + \sin \frac x 2}{\cos \frac x 2 - \sin \frac x 2} \times \frac {\cos \frac x 2 + \sin \frac x 2}{\cos \frac x 2 + \sin \frac x 2}
}}
{{eqn | r = \frac{\cos^2 \frac x 2 + \sin^2 \frac x 2 + 2 \cos \frac x 2 \sin \frac x 2}{\cos^2 \frac x 2 - \sin^2 \frac x 2}
}}
{{eqn | r = \frac{1 + 2 \cos \frac x 2 \sin \frac x 2}{\cos^2 \frac x 2 - \sin^2 \frac x 2}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \frac{1 + \sin x}{\cos x}
      | c = Double Angle Formula for Sine, Double Angle Formula for Cosine
}}
{{eqn | r = \sec x + \tan x
      | c = Sum of Secant and Tangent
}}
{{end-eqn}}
{{qed}}
Category:Trigonometric Identities
2ylde7dt30nahj4y1u0pwz17afz24fx
Theorem: Primitive of Power of Cosecant of a x

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

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

Proof:
{{begin-eqn}}
{{eqn | l = \int \csc x \rd x
      | r = \ln \size {\tan \frac x 2}
      | c = Primitive of $\csc x$: Tangent Form
}}
{{eqn | ll= \leadsto
      | l = \int \csc a x \rd x
      | r = \frac 1 a \ln \size {\tan \frac {a x} 2} + C
      | c = Primitive of Function of Constant Multiple
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Cosecant of a x/Cosecant minus Cotangent Form

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

Proof:
{{begin-eqn}}
{{eqn | l = \int \csc x \rd x
      | r = \ln \size {\csc x - \cot x}
      | c = Primitive of $\csc x$: Cosecant minus Cotangent Form
}}
{{eqn | ll= \leadsto
      | l = \int \csc a x \rd x
      | r = \frac 1 a \ln \size {\csc a x - \cot a x} + C
      | c = Primitive of Function of Constant Multiple
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of Square of 1 plus Sine of a x

:$\ds \int \frac {\d x} {\paren {1 + \sin a x}^2} = \frac {-1} {2 a} \map \tan {\frac \pi 4 - \frac {a x} 2} - \frac 1 {6 a} \map {\tan^3} {\frac \pi 4 - \frac {a x} 2} + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {\paren {1 + \sin a x}^2}
      | r = \int \paren {\frac 1 2 \map {\sec^2} {\dfrac \pi 4 - \frac {a x} 2} }^2 \rd x
      | c = Reciprocal of One Plus Sine
}}
{{eqn | r = \frac 1 4 \int \map {\sec^4} {\frac \pi 4 - \frac {a x} 2} \rd x
      | c = simplifying
}}
{{end-eqn}}
Let:
{{begin-eqn}}
{{eqn | l = z
      | r = \frac \pi 4 - \frac {a x} 2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d z} {\ d x}
      | r = \frac {-a} 2
      | c = simplifying
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \frac 1 4 \int \map {\sec^4} {\frac \pi 4 - \frac {a x} 2} \rd x
      | r = \frac 1 4 \int \frac {-2} a \sec^4 z \rd z
      | c = Integration by Substitution
}}
{{eqn | r = \frac {-1} {2 a} \int \sec^4 z \rd z
      | c = simplifying
}}
{{eqn | r = \frac {-1} {2 a} \paren {\frac {\sec^2 z \tan z} 3 + \frac 2 3 \int \sec^2 z \rd z} + C
      | c = Primitive of $\sec^n a x$
}}
{{eqn | r = \frac {-1} {2 a} \paren {\frac {\sec^2 z \tan z} 3 + \frac 2 3 \tan z} + C
      | c = Primitive of $\sec^2 a x$
}}
{{eqn | r = \frac {-1} {2 a} \paren {\frac {\paren {1 + \tan^2 z} \tan z} 3 + \frac 2 3 \tan z} + C
      | c = Difference of Squares of Secant and Tangent
}}
{{eqn | r = \frac {-1} {2 a} \tan z - \frac 1 {6 a} \tan^3 z + C
      | c = simplifying
}}
{{eqn | r = \frac {-1} {2 a} \map \tan {\frac \pi 4 - \frac {a x} 2} - \frac 1 {6 a} \map {\tan^3} {\frac \pi 4 - \frac {a x} 2} + C
      | c = substituting for $z$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of p plus q by Sine of a x

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

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {p + q \sin a x}
      | r =  \frac 2 a \int \frac {\d u} {p u^2 + 2 q u + p}
      | c = Weierstrass Substitution: $u = \tan \dfrac {a x} 2$
}}
{{end-eqn}}
The discriminant of $p u^2 + 2 q u + p$ is $4 q^2 - 4 p^2$.
Thus:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {p + q \sin a x}
      | r = \begin{cases} 
\ds \frac 2 a \paren {\dfrac 2 {\sqrt {4 p^2 - 4 q^2} } \map \arctan {\dfrac {2 p u + 2 q} {\sqrt {4 p^2 - 4 q^2} } } } + C & : 4 q^2 - 4 p^2 < 0 \\
\ds \frac 2 a \paren {\dfrac 1 {\sqrt {4 q^2 - 4 p^2} } \ln \size {\dfrac {2 p x + 2 q - \sqrt {4 q^2 - 4 p^2} } {2 p x + 2 q + \sqrt {4 q^2 - 4 p^2} } } } + C & : 4 q^2 - 4 p^2 > 0 \\
\end{cases}
      | c = Primitive of $\dfrac 1 {a x^2 + b x + c}$
}}
{{eqn | r = \begin{cases} 
\ds \dfrac 2 {a \sqrt {p^2 - q^2} } \map \arctan {\dfrac {p u + q} {\sqrt {p^2 - q^2} } } + C & : q^2 - p^2 < 0 \\
\ds \dfrac 1 {a \sqrt {q^2 - p^2} } \ln \size {\dfrac {p x + q - \sqrt {q^2 - p^2} } {p x + q + \sqrt {q^2 - p^2} } } + C & : q^2 - p^2 > 0 \\
\end{cases}
      | c = simplifying
}}
{{eqn | r = \begin{cases} 
\ds \frac 2 {a \sqrt {p^2 - q^2} } \map \arctan {\frac {p \tan \dfrac {a x} 2 + q} {\sqrt {p^2 - q^2} } } + C & : q^2 - p^2 < 0 \\
\ds \frac 1 {a \sqrt {q^2 - p^2} } \ln \size {\frac {p \tan \dfrac {a x} 2 + q - \sqrt {p^2 - q^2} } {p \tan \dfrac {a x} 2 + q + \sqrt {p^2 - q^2} } } + C & : q^2 - p^2 > 0 \\
\end{cases}
      | c = substituting for $u$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of p squared plus square of q by Sine of a x

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

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {p^2 + q^2 \sin^2 a x}
      | r = \int \frac {\sec^2 a x \rd x} {p^2 \sec^2 a x + q^2 \tan^2 a x}
      | c = multiplying numerator and denominator by $\sec^2 a x$
}}
{{eqn | r = \int \frac {\sec^2 a x \rd x} {p^2 + \paren {p^2 + q^2} \tan^2 a x}
      | c = Difference of Squares of Secant and Tangent
}}
{{eqn | r = \int \frac {\paren {\tan a x}' \rd x} {a p^2 + a \paren {p^2 + q^2} \tan^2 a x}
      | c = Derivative of Tangent Function
}}
{{eqn | r = \int \frac {\d t} {a p^2 + a \paren {p^2 + q^2} t^2}
      | c = substituting $t = \tan 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} \tan a x} p} + C
      | c = substituting $t = \tan a x$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power of x by Sine of a x

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

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

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

Proof:
With a view to expressing the primitive in the form:
:$\ds \int u \frac {\rd v} {\rd x} \rd x = u v - \int v \frac {\rd u} {\rd x} \rd x$
let:
{{begin-eqn}}
{{eqn | l = u
      | r = \sin a x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = a \cos a x
      | c = Derivative of $\sin 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 {\sin a x} {x^n} \rd x
      | r = \sin a x \paren {\frac {-1} {\paren {n - 1} x^{n - 1} } } - \int \paren {\frac {-1} {\paren {n - 1} x^{n - 1} } } \paren {a \cos a x} \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = \frac {-\sin a x} {\paren {n - 1} x^{n - 1} } + \frac a {n - 1} \int \frac {\cos a x} {x^{n - 1} } \rd x
      | c = Primitive of Constant Multiple of Function
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of Power of Sine of a x

:$\ds \int \frac {\d x} {\sin^n a x} = \frac {-\cos a x} {a \paren {n - 1} \sin^{n - 1} a x} + \frac {n - 2} {n - 1} \int \frac {\d x} {\sin^{n - 2} a 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 = \frac 1 {\sin^{n - 2} a x}
      | c = 
}}
{{eqn | r = \sin^{- n + 2} a x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = a \paren {-n + 2} \sin^{-n + 1} a x \cos a x
      | c = Derivative of $\sin a x$, Derivative of Power, Chain Rule for Derivatives
}}
{{eqn | r = \frac {-a \paren {n - 2} \cos a x} {\sin^{n - 1} a x}
      | c = simplifying
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = \frac 1 {\sin^2 a x}
      | c = 
}}
{{eqn | r = \csc^2 a x
      | c = Cosecant is $\dfrac 1 \sin$
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {-\cot a x} a
      | c = Primitive of $\csc^2 a x$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {\sin^n a x}
      | r = \int \frac {\d x} {\sin^{n - 2} a x \sin^2 a x}
      | c = 
}}
{{eqn | r = \paren {\frac 1 {\sin^{n - 2} a x} } \paren {\frac {-\cot a x} a} - \int \paren {\frac {-\cot a x} a} \paren {\frac {-a \paren {n - 2} \cos a x} {\sin^{n - 1} a x} } \rd x
      | c = Integration by Parts
}}
{{eqn | r = \frac {-\cos a x} {a \sin^{n - 1} a x} - \int \frac {\paren {n - 2} \cos^2 a x} {\sin^n a x} \rd x
      | c = Cotangent is $\dfrac {\cos} {\sin}$
}}
{{eqn | r = \frac {-\cos a x} {a \sin^{n - 1} a x} - \int \frac {\paren {n - 2} \paren {1 - \sin^2 a x} } {\sin^n a x} \rd x
      | c = Sum of $\sin^2$ and $\cos^2$
}}
{{eqn | r = \frac {-\cos a x} {a \sin^{n - 1} a x} - \paren {n - 2} \int \frac {\d x} {\sin^n a x} + \paren {n - 2} \int \frac {\d x} {\sin^{n - 2} a x}
      | c = Linear Combination of Primitives
}}
{{eqn | ll= \leadsto
      | l = \paren {n - 1} \int \frac {\d x} {\sin^n a x}
      | r = \frac {-\cos a x} {a \sin^{n - 1} a x} + \paren {n - 2} \int \frac {\d x} {\sin^{n - 2} a x}
      | c = gathering terms
}}
{{eqn | ll= \leadsto
      | l = \int \frac {\d x} {\sin^n a x}
      | r = \frac {-\cos a x} {a \paren {n - 1} \sin^{n - 1} a x} + \frac {n - 2} {n - 1} \int \frac {\d x} {\sin^{n - 2} a x}
      | c = dividing by $n - 1$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of x by Cosine of a x

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

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

:$\ds \int x^3 \map \cos {a x} \rd x = \paren {\frac {3 x^2} {a^2} - \frac 6 {a^4} } \cos a x + \paren {\frac {x^3} a - \frac {6 x} {a^3} } \sin 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^3
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = 3 x^2
      | c = Derivative of Power
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = \cos a x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {\sin a x} a
      | c = Primitive of $\cos a x$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int x^3 \map \cos {a x} \rd x
      | r = x^3 \paren {\frac {\sin a x} a} - \int \paren {3 x^2 \frac {\sin a x} a} \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = \frac {x^3 \sin a x} a - \frac 3 a \int x^2 \sin a x \rd x + C
      | c = Linear Combination of Primitives
}}
{{eqn | r = \frac {x^3 \sin a x} a - \frac 3 a \paren {\frac {2 x \sin a x} {a^2} + \paren {\frac 2 {a^3} - \frac {x^2} a} \cos a x} + C
      | c = Primitive of $x^2 \sin a x$
}}
{{eqn | r = \paren {\frac {3 x^2} {a^2} - \frac 6 {a^4} } \cos a x + \paren {\frac {x^3} a - \frac {6 x} {a^3} } \sin a x + C
      | c = simplification
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Cosine of a x over x squared

:$\ds \int \frac {\cos a x \rd x} {x^2} = \frac {-\cos a x} x - a \int \frac {\sin a x \rd x} 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^2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = - \frac 1 x
      | c = Primitive of Power
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \frac {\cos a x \rd x} {x^2}
      | r = \int \cos a x \frac 1 {x^2} \rd x
      | c = 
}}
{{eqn | r = \cos a x \paren {-\frac 1 x} - \int \paren {-\frac 1 x} \paren {-a \sin a x} \rd x
      | c = Integration by Parts
}}
{{eqn | r = \frac {-\cos a x} x - a \int \frac {\sin a x \rd x} x
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of Cosine of a x/Logarithm of Secant plus Tangent Form

:$\ds \int \frac {\d x} {\cos a x} = \frac 1 a \ln \size {\sec a x + \tan a z}$

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {\cos x}
      | r = \int \sec x \rd x
      | c = {{Defof|Real Secant Function}}
}}
{{eqn | r = \ln \size {\sec x + \tan x} + C
      | c = Primitive of $\sec x$: Secant plus Tangent Form
}}
{{eqn | ll= \leadsto
      | l = \int \frac {\d x} {\cos a 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 Reciprocal of Cosine of a x/Logarithm of Tangent Form

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

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {\cos x}
      | r = \int \sec x \rd x
      | c = {{Defof|Real Secant Function}}
}}
{{eqn | r = \ln \size {\map \tan {\frac \pi 4 + \frac x 2} } + C
      | c = Primitive of $\sec x$: Tangent plus Angle Form
}}
{{eqn | ll= \leadsto
      | l = \int \frac {\d x} {\cos a 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 x over Cosine of a x

{{begin-eqn}}
{{eqn | l = \int \frac {x \rd x} {\cos a x}
      | r = \frac 1 {a^2} \sum_{n \mathop = 0}^\infty \frac {E_n \paren {a x}^{2 n + 2} } {\paren {2 n + 2} \paren {2 n}!} + C
      | c = 
}}
{{eqn | r = \dfrac 1 {a^2} \paren {\frac {\paren {a x}^2} 2 + \frac {\paren {a x}^4} 8 + \frac {5 \paren {a x}^6} {144} + \cdots} + C
      | c = 
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn 	| l = \int \frac {x \rd x}{\cos a x} 
	| r = \int x \sec a x \rd x
	| c = {{Defof|Secant Function}}
}}
{{eqn 	| r = \frac 1 {a^2} \sum_{n \mathop = 0}^\infty \frac {E_n \paren {a x}^{2 n + 2} } {\paren {2 n + 2} \paren {2 n}!} + C
	| c = Primitive of $x \sec a x$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Square of Cosine of a x

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

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

:$\ds \int x \cos^2 a x \rd x = \frac {x^2} 4 + \frac {x \sin 2 a x} {4 a} + \frac {\cos 2 a x} {8 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
      | 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 = \cos^2 a x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac x 2 + \frac {\sin 2 a x} {4 a}
      | c = Primitive of $\cos^2 a x$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int x \cos^2 a x \rd x
      | r = x \paren {\frac x 2 + \frac {\sin 2 a x} {4 a} } - \int \paren {\frac x 2 + \frac {\sin 2 a x} {4 a} } \times 1 \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = \frac {x^2} 2 + \frac {x \sin 2 a x} {4 a} - \frac 1 2 \int x \rd x - \frac 1 {4 a} \int \sin 2 a x \rd x + C
      | c = Linear Combination of Primitives
}}
{{eqn | r = \frac {x^2} 2 + \frac {x \sin 2 a x} {4 a} - \frac {x^2} 4 - \frac 1 {4 a} \int \sin 2 a x \rd x + C
      | c = Primitive of Power
}}
{{eqn | r = \frac {x^2} 2 + \frac {x \sin 2 a x} {4 a} - \frac {x^2} 4 - \frac 1 {4 a} \frac {\paren {-\cos 2 a x} } {2 a} + C
      | c = Primitive of $\sin a x$
}}
{{eqn | r = \frac {x^2} 4 + \frac {x \sin 2 a x} {4 a} + \frac {\cos 2 a x} {8 a^2} + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}