avewright/proofwiki-math huggingface dataset:
Theorem: Primitive of Reciprocal of p squared by square of Sine of a x plus q squared by square of Cosine of a x

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

Proof:
Let $u = p^2 + q^2$ and $v = q^2 - p^2$.
Then:
{{begin-eqn}}
{{eqn | n = 1
      | l = u + v
      | r = 2 q^2
}}
{{eqn | n = 2
      | l = u - v
      | r = 2 p ^2
}}
{{end-eqn}}
Also:
{{begin-eqn}}
{{eqn | l = u^2 - v^2
      | r = \paren {u + v} \paren {u - v}
}}
{{eqn | l = u^2 - v^2
      | r = \paren {2 q^2} \paren {2 p^2}
      | c = from $\paren 1$ and $\paren 2$
}}
{{eqn | n = 3
      | l = u^2 - v^2
      | r = 4 p^2 q^2
}}
{{end-eqn}}
Therefore:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {p^2 \sin^2 a x + q^2 \cos^2 a x}
      | r = \int \frac {\d x} {p^2 \paren {\frac {1 - \cos 2 a x} 2} + q^2 \cos^2 a x}
      | c = Square of Sine
}}
{{eqn | r = \int \frac {\d x} {p^2 \paren {\frac {1 - \cos 2 a x} 2} + q^2 \paren {\frac {1 + \cos 2 a x} 2} }
      | c = Square of Cosine
}}
{{eqn | r = \int \frac {2 \d x} {p^2 - p^2 \cos 2 a x + q^2 + q^2 \cos 2 a x}
      | c = 
}}
{{eqn | r = \int \frac {2 \d x} {p^2 + q^2 + \paren {q^2 - p^2} \cos 2 a x}
      | c = 
}}
{{eqn | r = 2 \paren { \frac 2 {\paren {2 a} \sqrt{u^2 - v^2} } } \map \arctan {\sqrt{ \frac {u - v} {u + v} } \tan \frac {\paren {2 a} x} 2} + C
      | c = Primitive of $\dfrac 1 {p + q \cos a x}$
}}
{{eqn | r = 2 \paren {\frac 1 {a \sqrt{4 p^2 q^2} } } \map \arctan {\sqrt{ \frac {2 p^2} {2 q^2} } \tan a x} + C
      | c = from $\paren 3$
}}
{{eqn | r = \paren {\frac 2 {2 a p q} } \map \arctan {\sqrt{ \frac {p^2} {q^2} } \tan a x} + C
      | c = 
}}
{{eqn | r = \paren {\frac 1 {a p q} } \map \arctan {\frac p q \tan a x} + C
      | c = 
}}
{{eqn | r = \frac 1 {a p q} \map \arctan {\frac {p \tan a x} q} + C
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of p squared by square of Sine of a x plus q squared by square of Cosine of a x

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

Proof:
{{begin-eqn}}
{{eqn	| l = \int \frac {\d x} {p^2 \sin^2 a x + q^2 \cos^2 a x}
	| r = \int \frac {\sec^2 a x \d x} {p^2 \tan^2 a x + q^2}
	| c = multiplying by $\dfrac {\sec^2 a x} {\sec^2 a x}$
}}
{{eqn	| r = \frac 1 a \int \frac {\d t} {p^2 t^2 + q^2}
	| c = substituting $t = \tan a x$
}}
{{eqn	| r = \frac 1 {a p^2} \int \frac {\d t} {t^2 + \paren {\frac q p}^2}
}}
{{eqn	| r = \frac 1 {a p^2} \times \frac p q \map \arctan {\frac {p t} q} + C
	| c = Primitive of $\dfrac 1 {x^2 + a^2}$
}}
{{eqn	| r = \frac 1 {a p q} \map \arctan {\frac {p \tan a x} q} + C
	| c = substituting back for $t$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of p squared by square of Sine of a x minus q squared by square of Cosine of a x

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

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {p^2 \sin^2 a x - q^2 \cos^2 a x}
      | r = \int \frac {\sec^2 a x} {p^2 \tan^2 a x - q^2} \rd x
      | c = multiplying by $\dfrac {\sec^2 a x} {\sec^2 a x}$
}}
{{eqn | r = \frac 1 a \int \frac 1 {p^2 t^2 - q^2} \rd t
      | c = substituting $t = \tan a x$
}}
{{eqn | r = \frac 1 {a p^2} \int \frac 1 {t^2 - \paren {\frac q p}^2} \rd t
}}
{{eqn | r = \frac 1 {2 a \frac {p^2} p q} \ln \size {\frac {t - \frac q p} {t + \frac q p} } + C
      | c = Primitive of $\dfrac 1 {x^2 - a^2}$: Logarithm Form
}}
{{eqn | r = \frac 1 {2 a p q} \ln \size {\frac {p t - q} {p t + q} } + C
}}
{{eqn | r = \frac 1 {2 a p q} \ln \size {\frac {p \tan a x - q} {p \tan a x + q} } + C
      | c = substituting back for $t$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power of Sine of a x by Power of Cosine of a x/Reduction of Power of Sine

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

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 = \sin^{m - 1} a x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = a \paren {m - 1} \sin^{m - 2} a x \cos a x
      | c = Derivative of $\sin a x$, Derivative of Power, Chain Rule for Derivatives
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = \sin a x \cos^n a x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {-\cos^{n + 1} a x} {\paren {n + 1} a}
      | c = Primitive of $\cos^n a x \sin a x$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \sin^m a x \cos^n a x \rd x
      | r = \int \paren {\sin^{m - 1} a x} \paren {\sin a x \cos^n a x} \rd v
      | c = 
}}
{{eqn | r = \paren {\sin^{m - 1} a x} \paren {\frac {-\cos^{n + 1} a x} {\paren {n + 1} a} }
      | c = Integration by Parts
}}
{{eqn | o = 
      | ro= -
      | r = \int \paren {\frac {-\cos^{n + 1} a x} {\paren {n + 1} a} } \paren {a \paren {m - 1} \sin^{m - 2} a x \cos a x} \rd x + C
      | c = 
}}
{{eqn | r = \frac {-\sin^{m - 1} a x \cos^{n + 1} a x} {a \paren {n + 1} } + \frac {m - 1} {n + 1} \int \sin^{m - 2} a x \cos^{n + 2} a x \rd x + C
      | c = simplifying
}}
{{eqn | r = \frac {-\sin^{m - 1} a x \cos^{n + 1} a x} {a \paren {n + 1} }
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = \frac {m - 1} {n + 1} \int \sin^{m - 2} a x \cos^n a x \paren {1 - \sin^2 a x} \rd x + C
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \frac {-\sin^{m - 1} a x \cos^{n + 1} a x} {a \paren {n + 1} } + \frac {m - 1} {n + 1} \int \sin^{m - 2} a x \cos^n a x \rd x
      | c = Linear Combination of Primitives
}}
{{eqn | o = 
      | ro= -
      | r = \frac {m - 1} {n + 1} \int \sin^m a x \cos^n a x \rd x + C
      | c = 
}}
{{end-eqn}}
Hence after rearranging:
{{begin-eqn}}
{{eqn | r = \frac {-\sin^{m - 1} a x \cos^{n + 1} a x} {a \paren {n + 1} } + \frac {m - 1} {n + 1} \int \sin^{m - 2} a x \cos^n a x \rd x
      | o = 
      | c = 
}}
{{eqn | r = \int \sin^m a x \cos^n a x \rd x + \frac {m - 1} {n + 1} \int \sin^m a x \cos^n a x \rd x + C
      | c = 
}}
{{eqn | r = \frac {n + 1} {n + 1} \int \sin^m a x \cos^n a x \rd x + \frac {m - 1} {n + 1} \int \sin^m a x \cos^n a x \rd x + C
      | c = common denominator
}}
{{eqn | r = \frac {m + n} {n + 1} \int \sin^m a x \cos^n a x \rd x + C
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \int \sin^m a x \cos^n a x \rd x
      | r = \frac {-\sin^{m - 1} a x \cos^{n + 1} a x} {a \paren {m + n} } + \frac {m - 1} {m + n} \int \sin^{m - 2} a x \cos^n a x \rd x + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power of Sine of a x by Power of Cosine of a x/Reduction of Power of Cosine

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

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^{n - 1} a x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = -a \paren {n - 1} \cos^{n - 2} a x \sin a x
      | c = Derivative of $\cos a x$, Derivative of Power, Chain Rule for Derivatives
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = \sin^m a x \cos a x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {\sin^{m + 1} a x} {\paren {m + 1} a}
      | c = Primitive of $\sin^n a x \cos a x$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \sin^m a x \cos^n a x \rd x
      | r = \int \paren {\cos^{n - 1} a x} \paren {\sin^m a x \cos a x} \rd v
      | c = 
}}
{{eqn | r = \paren {\cos^{n - 1} a x} \paren {\frac {\sin^{m + 1} } {\paren {m + 1} a} }
      | c = Integration by Parts
}}
{{eqn | o = 
      | ro= -
      | r = \int \paren {\frac {\sin^{m + 1} } {\paren {m + 1} a} } \paren {-a \paren {n - 1} \cos^{n - 2} a x \sin a x } \rd x + C
      | c = 
}}
{{eqn | r = \frac {\sin^{m + 1} a x \cos^{n - 1} a x} {a \paren {m + 1} } + \frac {n - 1} {m + 1} \int \sin^{m + 2} a x \cos^{n - 2} a x \rd x + C
      | c = simplifying
}}
{{eqn | r = \frac {\sin^{m + 1} a x \cos^{n - 1} a x} {a \paren {m + 1} }
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = \frac {n - 1} {m + 1} \int \sin^m a x \paren {1 - \cos^2 a x} \cos^{n - 2} a x \rd x + C
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \frac {\sin^{m + 1} a x \cos^{n - 1} a x} {a \paren {m + 1} } + \frac {n - 1} {m + 1} \int \sin^m a x \cos^{n - 2} a x \rd x
      | c = Linear Combination of Primitives
}}
{{eqn | o = 
      | ro= -
      | r = \frac {n - 1} {m + 1} \int \sin^m a x \cos^n a x \rd x + C
      | c = 
}}
{{end-eqn}}
Hence after rearranging:
{{begin-eqn}}
{{eqn | r = \frac {\sin^{m + 1} a x \cos^{n - 1} a x} {a \paren {m + 1} } + \frac {n - 1} {m + 1} \int \sin^m a x \cos^{n - 2} a x \rd x
      | o = 
      | c = 
}}
{{eqn | r = \int \sin^m a x \cos^n a x \rd x + \frac {n - 1} {m + 1} \int \sin^m a x \cos^n a x \rd x + C
      | c = 
}}
{{eqn | r = \frac {m + 1} {m + 1} \int \sin^m a x \cos^n a x \rd x + \frac {n - 1} {m + 1} \int \sin^m a x \cos^n a x \rd x + C
      | c = common denominator
}}
{{eqn | r = \frac {m + n} {m + 1} \int \sin^m a x \cos^n a x \rd x + C
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \int \sin^m a x \cos^n a x \rd x
      | r = \frac {\sin^{m + 1} a x \cos^{n - 1} a x} {a \paren {m + n} } + \frac {n - 1} {m + n} \int \sin^m a x \cos^{n - 2} a x \rd x + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power of Sine of a x over Power of Cosine of a x/Reduction of Both Powers

:$\ds \int \frac {\sin^m a x} {\cos^n a x} \rd x = \frac {\sin^{m - 1} a x} {a \paren {n - 1} \cos^{n - 1} a x} - \frac {m - 1} {n - 1} \int \frac {\sin^{m - 2} a x} {\cos^{n - 2} a 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 = \sin^{m - 1} a x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = \paren {m - 1} a \sin^{m - 2} a x \cos a x
      | c = Derivative of $\sin a x$, Derivative of Power, Chain Rule for Derivatives
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = \frac {\sin a x} {\cos^n a x}
      | c = 
}}
{{eqn | r = \cos^{-n} a x \sin a x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {-\cos^{-n + 1} a x} {a \paren {-n + 1} }
      | c = Primitive of $\cos^n a x \sin a x$
}}
{{eqn | r = \frac 1 {a \paren {n - 1} \cos^{n - 1} a x}
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \frac {\sin^m a x} {\cos^n a x} \rd x
      | r = \int \sin^{m - 1} a x \frac {\sin a x} {\cos^n a x} \rd x 
      | c = 
}}
{{eqn | r = \paren {\sin^{m - 1} a x} \paren {\frac 1 {a \paren {n - 1} \cos^{n - 1} a x} }
      | c = Integration by Parts
}}
{{eqn | o = 
      | ro= -
      | r = \int \paren {\frac 1 {a \paren {n - 1} \cos^{n - 1} a x} } \paren {\paren {m - 1} a \sin^{m - 2} a x \cos a x} \rd x + C
      | c = 
}}
{{eqn | r = \frac {\sin^{m - 1} a x} {a \paren {n - 1} \cos^{n - 1} a x} - \frac {m - 1} {n - 1} \int \frac {\sin^{m - 2} a x} {\cos^{n - 2} a x} \rd x + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power of Sine of a x over Power of Cosine of a x/Reduction of Power of Cosine

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

Proof:
{{begin-eqn}}
{{eqn | r = \frac {\sin^{m + 1} a x} {a \paren {n - 1} \cos^{n - 1} a x} - \frac {m + 1} {n - 1} \int \frac {\sin^m a x} {\cos^{n - 2} a x} \rd x + C
      | o = 
      | c = 
}}
{{eqn | r = \int \frac {\sin^{m + 2} a x} {\cos^n a x} \rd x
      | c = Primitive of $\dfrac {\sin^m a x} {\cos^n a x}$: Reduction of Both Powers
}}
{{eqn | r = \int \frac {\sin^m a x \paren {1 - \cos^2 a x} } {\cos^n a x} \rd x
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \int \frac {\sin^m a x} {\cos^n a x} \rd x - \int \frac {\sin^m a x \cos^2 a x} {\cos^n a x} \rd x
      | c = Linear Combination of Primitives
}}
{{eqn | r = \int \frac {\sin^m a x} {\cos^n a x} \rd x - \int \frac {\sin^m a x} {\cos^{n - 2} a x} \rd x
      | c = simplifying
}}
{{end-eqn}}
Hence, rearranging:
{{begin-eqn}}
{{eqn | l = \int \frac {\sin^m a x} {\cos^n a x} \rd x
      | r = \frac {\sin^{m + 1} a x} {a \paren {n - 1} \cos^{n - 1} a x} - \frac {m + 1} {n - 1} \int \frac {\sin^m a x} {\cos^{n - 2} a x} \rd x + \int \frac {\sin^m a x} {\cos^{n - 2} a x} \rd x + C
      | c = 
}}
{{eqn | r = \frac {\sin^{m + 1} a x} {a \paren {n - 1} \cos^{n - 1} a x} - \frac {m + 1} {n - 1} \int \frac {\sin^m a x} {\cos^{n - 2} a x} \rd x - \frac {-n + 1} {n - 1} \int \frac {\sin^m a x} {\cos^{n - 2} a x} \rd x + C
      | c = common denominator
}}
{{eqn | r = \frac {\sin^{m + 1} a x} {a \paren {n - 1} \cos^{n - 1} a x} - \frac {m - n + 2} {n - 1} \int \frac {\sin^m a x} {\cos^{n - 2} a x} \rd x + C
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power of Cosine of a x over Power of Sine of a x/Reduction of Both Powers

:$\ds \int \frac {\cos^m a x} {\sin^n a x} \rd x = \frac {-\cos^{m - 1} a x} {a \paren {n - 1} \sin^{n - 1} a x} - \frac {m - 1} {n - 1} \int \frac {\cos^{m - 2} a x} {\sin^{n - 2} a 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 = \cos^{m - 1} a x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = -\paren {m - 1} a \cos^{m - 2} a x \sin a x
      | c = Derivative of $\cos a x$, Derivative of Power, Chain Rule for Derivatives
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = \frac {\cos a x} {\sin^n a x}
      | c = 
}}
{{eqn | r = \sin^{-n} a x \cos a x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {\sin^{-n + 1} a x} {a \paren {-n + 1} }
      | c = Primitive of $\sin^n a x \cos a x$
}}
{{eqn | r = \frac {-1} {a \paren {n - 1} \sin^{n - 1} a x}
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \frac {\cos^m a x} {\sin^n a x} \rd x
      | r = \int \cos^{m - 1} a x \frac {\cos a x} {\sin^n a x} \rd x 
      | c = 
}}
{{eqn | r = \paren {\cos^{m - 1} a x} \paren {\frac {-1} {a \paren {n - 1} \sin^{n - 1} a x} }
      | c = Integration by Parts
}}
{{eqn | o = 
      | ro= -
      | r = \int \paren {\frac {-1} {a \paren {n - 1} \sin^{n - 1} a x} } \paren {-\paren {m - 1} a \cos^{m - 2} a x \sin a x } \rd x + C
      | c = 
}}
{{eqn | r = \frac {-\cos^{m - 1} a x} {a \paren {n - 1} \sin^{n - 1} a x} - \frac {m - 1} {n - 1} \int \frac {\cos^{m - 2} a x} {\sin^{n - 2} a x} \rd x + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power of Cosine of a x over Power of Sine of a x/Reduction of Power of Sine

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

Proof:
{{begin-eqn}}
{{eqn | r = \frac {-\cos^{m + 1} a x} {a \paren {n - 1} \sin^{n - 1} a x} - \frac {m + 1} {n - 1} \int \frac {\cos^m a x} {\sin^{n - 2} a x} \rd x + C
      | o = 
      | c = 
}}
{{eqn | r = \int \frac {\cos^{m + 2} a x} {\sin^n a x} \rd x
      | c = Primitive of $\dfrac {\cos^m a x} {\sin^n a x}$: Reduction of Both Powers
}}
{{eqn | r = \int \frac {\cos^m a x \paren {1 - \sin^2 a x} } {\sin^n a x} \rd x
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \int \frac {\cos^m a x} {\sin^n a x} \rd x - \int \frac {\cos^m a x \sin^2 a x} {\sin^n a x} \rd x
      | c = Linear Combination of Primitives
}}
{{eqn | r = \int \frac {\cos^m a x} {\sin^n a x} \rd x - \int \frac {\cos^m a x} {\sin^{n - 2} a x} \rd x
      | c = simplifying
}}
{{end-eqn}}
Hence, rearranging:
{{begin-eqn}}
{{eqn | l = \int \frac {\cos^m a x} {\sin^n a x} \rd x
      | r = \frac {-\cos^{m + 1} a x} {a \paren {n - 1} \sin^{n - 1} a x} - \frac {m + 1} {n - 1} \int \frac {\cos^m a x} {\sin^{n - 2} a x} \rd x + \int \frac {\cos^m a x} {\sin^{n - 2} a x} \rd x + C
      | c = 
}}
{{eqn | r = \frac {-\cos^{m + 1} a x} {a \paren {n - 1} \sin^{n - 1} a x} - \frac {m + 1} {n - 1} \int \frac {\cos^m a x} {\sin^{n - 2} a x} \rd x - \frac {-n + 1} {n - 1} \int \frac {\cos^m a x} {\sin^{n - 2} a x} \rd x + C
      | c = common denominator
}}
{{eqn | r = \frac {-\cos^{m + 1} a x} {a \paren {n - 1} \sin^{n - 1} a x} - \frac {m - n + 2} {n - 1} \int \frac {\cos^m a x} {\sin^{n - 2} a x} \rd x + C
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of Power of Cosine of a x by Power of Sine of a x/Reduction of Power of Cosine

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

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {\sin^m a x \cos^n a x}
      | r = \int \frac {\sin^{-m} a x \rd x} {\cos^n a x}
      | c = 
}}
{{eqn | r = \frac {\sin^{-m + 1} a x} {a \paren {n - 1} \cos^{n - 1} a x} - \frac {-m - n + 2} {n - 1} \int \frac {\sin^{-m} a x} {\cos^{n - 2} a x} \rd x + C
      | c = Primitive of $\dfrac {\sin^m a x} {\cos^n a x}$
}}
{{eqn | r = \frac 1 {a \paren {n - 1} \sin^{m - 1} a x \cos^{n - 1} a x} + \frac {m + n - 2} {n - 1} \int \frac {\d x} {\sin^m a x \cos^{n - 2} a x} + C
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of Power of Cosine of a x by Power of Sine of a x/Reduction of Power of Sine

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

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {\sin^m a x \cos^n a x}
      | r = \int \frac {\cos^{-n} a x \rd x} {\sin^m a x}
      | c = 
}}
{{eqn | r = \frac {-\cos^{-n + 1} a x} {a \paren {m - 1} \sin^{m - 1} a x} - \frac {-n - m + 2} {m - 1} \int \frac {\cos^{-n} a x} {\sin^{m - 2} a x} \rd x + C
      | c = Primitive of $\dfrac {\cos^m a x} {\sin^n a x}$
}}
{{eqn | r = \frac {-1} {a \paren {n - 1} \sin^{m - 1} a x \cos^{n - 1} a x} + \frac {m + n - 2} {m - 1} \int \frac {\d x} {\sin^{m - 2} a x \cos^n a x} + C
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Tangent of a x/Cosine Form

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

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

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

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

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

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

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

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

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

Proof:
{{begin-eqn}}
{{eqn | l = I_n
      | r = \int \map {\tan^n} {a x} \rd x
}}
{{eqn | r = \frac {\map {\tan^{n - 1} } {a x} } {a \paren {n - 1} } - I_{n - 2} 
      | c = Reduction Formula for Integral of Power of Tangent
}}
{{eqn | l = I_1
      | r = -\frac 1 a \ln \size {\map \cos {a x} } + C
      | c = Primitive of $\tan a x$: Cosine Form
}}
{{eqn | ll = \leadsto
      | l = I_3
      | r = \frac {\map {\tan^2} {a x} } {2 a} + \frac 1 a \ln \size {\map \cos {a x} } + C'
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power of Tangent of a x by Square of Secant of a x

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

Proof:
{{begin-eqn}}
{{eqn | l = z
      | r = \tan a x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d z} {\d x}
      | r = a \sec^2 a x
      | c = Derivative of $\tan a x$
}}
{{eqn | ll= \leadsto
      | l = \int \tan^n a x \sec^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 {\tan^{n + 1} a x} {\paren {n + 1} a} + C
      | c = substituting for $z$ and simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Cotangent of a x

:$\ds \int \cot a x \rd x = \frac {\ln \size {\sin a x} } a + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \cot x \rd x
      | r = \ln \size {\sin x}
      | c = Primitive of $\cot x$
}}
{{eqn | ll= \leadsto
      | l = \int \cot a x \rd x
      | r = \frac 1 a \paren {\ln \size {\sin a x} } + C
      | c = Primitive of Function of Constant Multiple
}}
{{eqn | r = \frac {\ln \size {\sin a x} } a + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of Tangent of a x

:$\ds \int \frac {\d x} {\tan a x} = \frac 1 a \ln \size {\sin a x} + C$

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