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

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

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

Proof:
{{begin-eqn}}
{{eqn | l = \int \sin a x \cos a x \rd x
      | r = \int \frac {\sin 2 a x} 2 \rd x
      | c = Double Angle Formula for Sine
}}
{{eqn | r = \frac {-\cos 2 a x} {4 a} + C
      | c = Primitive of $\cos a x$
}}
{{eqn | r = \frac {-\paren {1 - 2 \sin^2 a x} } {4 a} + C
      | c = {{Corollary|Double Angle Formula for Cosine|2}}
}}
{{eqn | r = \frac {-1} {4 a} + \frac {\sin^2 a x} {2 a} + C
      | c = separating fraction
}}
{{eqn | r = \frac {\sin^2 a x} {2 a} + C
      | c = subsuming $\dfrac {-1} {4 a}$ into arbitrary constant
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Sine of a x by Cosine of b x

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

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

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

Proof:
{{begin-eqn}}
{{eqn | l = z
      | r = \sin a x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d z} {\d x}
      | r = a \cos a x
      | c = Primitive of $\sin a x$
}}
{{eqn | ll= \leadsto
      | l = \int \sin^n a x \cos a x \rd x
      | r = \int \frac {z^n \rd x} a
      | c = Integration by Substitution
}}
{{eqn | r = \frac {z^{n + 1} } {\paren {n + 1} a} + C
      | c = Primitive of Power
}}
{{eqn | r = \frac {\sin^{n + 1} a x} {\paren {n + 1} a} + C
      | c = substituting for $z$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power of Cosine of a x by Sine of a x

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

Proof:
{{begin-eqn}}
{{eqn | l = z
      | r = \cos a x
      | c = Werner Formula for Sine by Cosine
}}
{{eqn | ll= \leadsto
      | l = \frac {\d z} {\d x}
      | r = -a \sin a x
      | c = Primitive of $\cos a x$
}}
{{eqn | ll= \leadsto
      | l = \int \cos^n a x \sin a x \rd x
      | r = \int \frac {-z^n \rd x} a
      | c = Integration by Substitution
}}
{{eqn | r = \frac {-z^{n + 1} } {\paren {n + 1} a} + C
      | c = Primitive of Power
}}
{{eqn | r = \frac {-\cos^{n + 1} a x} {\paren {n + 1} a} + C
      | c = substituting for $z$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Sine of a x squared by Cosine of a x squared

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

Proof:
{{begin-eqn}}
{{eqn | l = \int \sin^2 a x \cos^2 a x \rd x
      | r = \int \sin^2 a x \paren {1 - \sin^2 a x} \rd x
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \int \sin^2 a x \rd x - \int \sin^4 a x \rd x
      | c = Linear Combination of Primitives
}}
{{eqn | r = \frac x 2 - \frac {\sin 2 a x} {4 a} - \int \sin^4 a x \rd x + C
      | c = Primitive of $\sin^2 a x$
}}
{{eqn | r = \frac x 2 - \frac {\sin 2 a x} {4 a} - \paren {\frac {3 x} 8 - \frac {\sin 2 a x} {4 a} + \frac {\sin 4 a x} {32 a} } + C
      | c = Primitive of $\sin^4 a x$
}}
{{eqn | r = \frac x 8 - \frac {\sin 4 a x} {32 a} + C
      | c = gathering terms and simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Sine of a x squared by Cosine of a x squared

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

Proof:
{{begin-eqn}}
{{eqn	| l = \int \sin^2 a x \cos^2 a x \rd x
	| r = \int \paren {\sin a x \cos a x}^2 \rd x
}}
{{eqn	| r = \int \paren {\frac 1 2 \sin 2 a x}^2 \rd x
	| c = Double Angle Formula for Sine
}}
{{eqn	| r = \frac 1 4 \int \sin^2 2 a x \rd x
}}
{{eqn	| r = \frac 1 4 \paren {\frac x 2 - \frac {\map \sin {2 x \times 2 a} } {4 \times 2 a} } + C
	| c = Primitive of $\sin^2 a x$
}}
{{eqn	| r = \frac x 8 - \frac {\sin 4 a x} {32 a} + C
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of Sine of x by Cosine of x/Corollary

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

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

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

Proof:
{{begin-eqn}}
{{eqn | l = \frac {\d} {\d x} \tan x
      | r = \sec^2 x
      | c = Derivative of Tangent Function
}}
{{eqn | ll= \leadsto
      | l = \int \frac {\sec^2 x \rd x} {\tan x}
      | r = \ln \size {\tan a x} + C
      | c = Primitive of Function under its Derivative
}}
{{eqn | ll= \leadsto
      | l = \int \frac {\sec^2 a x \rd x} {\tan a x}
      | r = \frac 1 a \ln \size {\tan a x} + C
      | c = Primitive of Function of Constant Multiple
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of Square of Sine of a x by Cosine of a x

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

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {\sin^2 a x \cos a x}
      | r = \int \frac {\paren {\sin^2 a x + \cos^2 a x} \rd x} {\sin^2 a x \cos a x}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \int \frac {\sin^2 a x \rd x} {\sin^2 a x \cos a x} + \int \frac {\cos^2 a x \rd x} {\sin^2 a x \cos a x}
      | c = Linear Combination of Primitives
}}
{{eqn | r = \int \frac {\d x} {\cos a x} + \int \frac {\cos a x \rd x} {\sin^2 a x}
      | c = simplifying
}}
{{eqn | r = \int \sec a x \rd x + \int \frac {\cos a x \rd x} {\sin^2 a x}
      | c = Secant is Reciprocal of Cosine
}}
{{eqn | r = \int \sec a x \rd x + \int \frac {\cot a x \rd x} {\sin a x}
      | c = Cotangent is Cosine divided by Sine
}}
{{eqn | r = \int \sec a x \rd x + \int \csc a x \cot a x \rd x
      | c = Cosecant is Reciprocal of Sine
}}
{{eqn | r = \frac 1 a \ln \size {\map \tan {\frac \pi 4 + \frac {a x} 2} } + \int \csc a x \cot a x \rd x + C
      | c = Primitive of $\sec a x$
}}
{{eqn | r = \frac 1 a \ln \size {\map \tan {\frac \pi 4 + \frac {a x} 2} } - \frac 1 {a \sin a x} + C
      | c = Primitive of $\csc^n a x \cot a x$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power of Cosecant of a x by Cotangent of a x

:$\ds \int \csc^n a x \cot a x \rd x = \frac {-\csc^n a x} {n a} + C$
for $n \ne 0$.

Proof:
{{begin-eqn}}
{{eqn | l = z
      | r = \csc a x
      | c =
}}
{{eqn | ll= \leadsto
      | l = \frac {\d z} {\d x}
      | r = -a \csc a x \cot a x
      | c = Derivative of Cosecant Function, Chain Rule for Derivatives
}}
{{eqn | ll= \leadsto
      | l = \int \csc^n a x \cot a x \rd x
      | r = \int \frac {-z^{n - 1} \rd z} a
      | c = Integration by Substitution
}}
{{eqn | r = \frac {-z^n} {n a}
      | c = Primitive of Power
}}
{{eqn | r = \frac {-\csc^n a x} {n a} + C
      | c = substituting for $z$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of Sine of a x by Square of Cosine of a x

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

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {\sin a x \cos^2 a x}
      | r = \int \frac {\paren {\sin^2 a x + \cos^2 a x} \rd x} {\sin a x \cos^2 a x}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \int \frac {\sin^2 a x \rd x} {\sin a x \cos^2 a x} + \int \frac {\cos^2 a x \rd x} {\sin a x \cos^2 a x}
      | c = Linear Combination of Primitives
}}
{{eqn | r = \int \frac {\d x} {\sin a x} + \int \frac {\sin a x \rd x} {\cos^2 a x}
      | c = simplifying
}}
{{eqn | r = \int \csc a x \rd x + \int \frac {\sin a x \rd x} {\cos^2 a x}
      | c = Cosecant is Reciprocal of Sine
}}
{{eqn | r = \int \csc a x \rd x + \int \frac {\tan a x \rd x} {\cos a x}
      | c = Tangent is Sine divided by Cosine
}}
{{eqn | r = \int \csc a x \rd x + \int \sec a x \tan a x \rd x
      | c = Secant is Reciprocal of Cosine
}}
{{eqn | r = \frac 1 a \ln \size {\tan \frac {a x} 2} + \int \sec a x \tan a x \rd x + C
      | c = Primitive of $\csc a x$
}}
{{eqn | r = \frac 1 a \ln \size {\tan \frac {a x} 2} + \frac 1 {a \cos a x} + C
      | c = Primitive of $\sec^n a x \tan a x$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power of Secant of a x by Tangent of a x

:$\ds \int \sec^n a x \tan a x \rd x = \frac {\sec^n a x} {n a} + C$
for $n \ne 0$.

Proof:
{{begin-eqn}}
{{eqn | l = z
      | r = \sec a x
      | c =
}}
{{eqn | ll= \leadsto
      | l = \frac {\d z} {\d x}
      | r = a \sec a x \tan a x
      | c = Derivative of Secant Function, Chain Rule for Derivatives
}}
{{eqn | ll= \leadsto
      | l = \int \sec^n a x \tan a x \rd x
      | r = \int \frac {z^{n - 1} \rd z} a
      | c = Integration by Substitution
}}
{{eqn | r = \frac {z^n} {n a}
      | c = Primitive of Power
}}
{{eqn | r = \frac {\sec^n a x} {n a} + C
      | c = substituting for $z$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of Square of Sine of a x by Square of Cosine of a x

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

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {\sin^2 a x \cos^2 a x}
      | r = \int \frac {\d x} {\left({\sin a x \cos a x}\right)^2}
      | c = 
}}
{{eqn | r = \int \frac {\d x} {\left({\frac {\sin 2 a x} 2}\right)^2}
      | c = Double Angle Formula for Sine
}}
{{eqn | r = 4 \int \frac {\d x} {\sin^2 2 a x}
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = 4 \int \csc^2 2 a x \rd x
      | c = Cosecant is Reciprocal of Sine
}}
{{eqn | r = 4 \frac {-\cot 2 a x} {2 a} + C
      | c = Primitive of Square of Cosecant of a x
}}
{{eqn | r = \frac {-2 \cot 2 a x} a + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Square of Sine of a x over Cosine of a x

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

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\sin^2 a x \rd x} {\cos a x}
      | r = \int \frac {\paren {1 - \cos^2 a x} \rd x} {\cos a x}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \int \frac {\d x} {\cos a x} - \int \cos a x \rd x
      | c = Linear Combination of Primitives
}}
{{eqn | r = \int \sec a x \rd x - \int \cos a x \rd x
      | c = Secant is Reciprocal of Cosine
}}
{{eqn | r = \frac {-\sin a x} a + \int \sec a x \rd x + C
      | c = Primitive of $\cos a x$
}}
{{eqn | r = \frac {-\sin a x} a + \frac 1 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 Square of Cosine of a x over Sine of a x

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

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\cos^2 a x \rd x} {\sin a x}
      | r = \int \frac {\paren {1 - \sin^2 a x} \rd x} {\sin a x}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \int \frac {\d x} {\sin a x} - \int \sin a x \rd x
      | c = Linear Combination of Primitives
}}
{{eqn | r = \int \csc a x \rd x - \int \sin a x \rd x
      | c = Cosecant is Reciprocal of Sine
}}
{{eqn | r = \frac {\cos a x} a + \int \csc a x \rd x + C
      | c = Primitive of $\sin a x$
}}
{{eqn | r = \frac {\cos a x} a + \frac 1 a \ln \size {\tan \frac {a x} 2} + C
      | c = Primitive of $\csc a x$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of Cosine of a x by 1 plus Sine of a x

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

Proof:
Let:
{{begin-eqn}}
{{eqn | l = u
      | r = \sin a x
      | c = 
}}
{{eqn | l = \frac {\d u} {\d x}
      | r = a \cos a x
      | c = Derivative of $\sin a x$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {\cos a x \paren {1 + \sin a x} } 
      | r = \int \frac {\cos a x \rd x} {\cos^2 a x \paren {1 + \sin a x} }
      | c = multiplying top and bottom by $\cos a x$
}}
{{eqn | r = \int \frac {\cos a x \rd x} {\paren {1 - \sin^2 a x} \paren {1 + \sin a x} }
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \frac 1 a \int \frac {\d u} {\paren {1 - u^2} \paren {1 + u} }
      | c = Integration by Substitution
}}
{{eqn | r = \frac 1 a \int \frac {\d u} {\paren {1 - u} \paren {1 + u}^2}
      | c = Difference of Two Squares
}}
{{eqn | r = \frac 1 a \paren {\frac 1 {-2} \paren {\frac 1 {1 + u} + \frac {-1} {-2} \ln \size {\frac {1 - u} {1 + u} } } } + C
      | c = Primitive of $\dfrac 1 {\paren {a x + b}^2 \paren {p x + q} }$
}}
{{eqn | r = \frac {-1} {2 a \paren {1 + u} } - \frac 1 {4 a} \ln \size {\frac {1 - u} {1 + u} } + C
      | c = simplifying
}}
{{eqn | r = \frac {-1} {2 a \paren {1 + \sin a x} } - \frac 1 {4 a} \ln \size {\frac {1 - \sin a x} {1 + \sin a x} } + C
      | c = substituting for $u$
}}
{{eqn | r = \frac {-1} {2 a \paren {1 + \sin a x} } - \frac 1 {4 a} \ln \size {\frac {\frac 1 2 \map {\sec^2} {\frac \pi 4 - \frac {a x} 2} } {\frac 1 2 \map {\sec^2} {\frac \pi 4 + \frac {a x} 2} } } + C
      | c = Reciprocal of $1 - \sin$ and Reciprocal of $1 + \sin$
}}
{{eqn | r = \frac {-1} {2 a \paren {1 + \sin a x} } - \frac 1 {4 a} \ln \size {\frac {\map {\cos^2} {\frac \pi 4 + \frac {a x} 2} } {\map {\cos^2} {\frac \pi 4 - \frac {a x} 2} } } + C
      | c = Secant is Reciprocal of Cosine
}}
{{eqn | r = \frac {-1} {2 a \paren {1 + \sin a x} } - \frac 1 {4 a} \ln \size {\frac {\map {\cos^2} {\frac \pi 4 + \frac {a x} 2} } {\map {\sin^2} {\frac \pi 2 - \paren {\frac \pi 4 - \frac {a x} 2} } } } + C
      | c = Sine of Complement equals Cosine
}}
{{eqn | r = \frac {-1} {2 a \paren {1 + \sin a x} } - \frac 1 {4 a} \ln \size {\frac {\map {\cos^2} {\frac \pi 4 + \frac {a x} 2} } {\map {\sin^2} {\frac \pi 4 + \frac {a x} 2} } } + C
      | c = 
}}
{{eqn | r = \frac {-1} {2 a \paren {1 + \sin a x} } + \frac 1 {4 a} \ln \size {\frac {\map {\sin^2} {\frac \pi 4 + \frac {a x} 2} } {\map {\cos^2} {\frac \pi 4 + \frac {a x} 2} } } + C
      | c = Logarithm of Reciprocal
}}
{{eqn | r = \frac {-1} {2 a \paren {1 + \sin a x} } + \frac 1 {4 a} \ln \size {\map {\tan^2} {\frac \pi 4 + \frac {a x} 2} } + C
      | c = Tangent is Sine divided by Cosine
}}
{{eqn | r = \frac {-1} {2 a \paren {1 + \sin a x} } + \frac 1 {2 a} \ln \size {\map \tan {\frac \pi 4 + \frac {a x} 2} } + C
      | c = Logarithm of Power
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of Cosine of a x by 1 minus Sine of a x

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

Proof:
Let:
{{begin-eqn}}
{{eqn | l = u
      | r = \sin a x
      | c = 
}}
{{eqn | l = \frac {\d u} {\d x}
      | r = a \cos a x
      | c = Derivative of $\sin a x$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {\cos a x \paren {1 - \sin a x} }
      | r = \int \frac {\cos a x \rd x} {\cos^2 a x \paren {1 - \sin a x} }
      | c = multiplying top and bottom by $\cos a x$
}}
{{eqn | r = \int \frac {\cos a x \rd x} {\paren {1 - \sin^2 a x} \paren {1 - \sin a x} }
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \frac 1 a \int \frac {\d u} {\paren {1 - u^2} \paren {1 - u} }
      | c = Integration by Substitution
}}
{{eqn | r = \frac 1 a \int \frac {\d u} {\paren {1 + u} \paren {1 - u}^2}
      | c = Difference of Two Squares
}}
{{eqn | r = \frac 1 a \paren {\frac 1 2 \paren {\frac 1 {1 - u} + \frac 1 2 \ln \size {\frac {1 + u} {1 - u} } } } + C
      | c = Primitive of $\dfrac 1 {\paren {a x + b}^2 \paren {p x + q} }$
}}
{{eqn | r = \frac 1 {2 a \paren {1 - u} } + \frac 1 {4 a} \ln \size {\frac {1 + u} {1 - u} } + C
      | c = simplifying
}}
{{eqn | r = \frac 1 {2 a \paren {1 - \sin a x} } + \frac 1 {4 a} \ln \size {\frac {1 + \sin a x} {1 - \sin a x} } + C
      | c = substituting for $u$
}}
{{eqn | r = \frac 1 {2 a \paren {1 - \sin a x} } + \frac 1 {4 a} \ln \size {\frac {\frac 1 2 \map {\sec^2} {\frac \pi 4 + \frac {a x} 2} } {\frac 1 2 \map {\sec^2} {\frac \pi 4 - \frac {a x} 2} } } + C
      | c = Reciprocal of $1 - \sin$ and Reciprocal of $1 + \sin$
}}
{{eqn | r = \frac 1 {2 a \paren {1 - \sin a x} } + \frac 1 {4 a} \ln \size {\frac {\map {\cos^2} {\frac \pi 4 - \frac {a x} 2} } {\map {\cos^2} {\frac \pi 4 + \frac {a x} 2} } } + C
      | c = Secant is Reciprocal of Cosine
}}
{{eqn | r = \frac 1 {2 a \paren {1 - \sin a x} } + \frac 1 {4 a} \ln \size {\frac {\map {\sin^2} {\frac \pi 2 - \paren {\frac \pi 4 - \frac {a x} 2} } } {\map {\cos^2} {\frac \pi 4 + \frac {a x} 2} } } + C
      | c = Sine of Complement equals Cosine
}}
{{eqn | r = \frac 1 {2 a \paren {1 - \sin a x} } + \frac 1 {4 a} \ln \size {\frac {\map {\sin^2} {\frac \pi 4 + \frac {a x} 2} } {\map {\cos^2} {\frac \pi 4 + \frac {a x} 2} } } + C
      | c = 
}}
{{eqn | r = \frac 1 {2 a \paren {1 - \sin a x} } + \frac 1 {4 a} \ln \size {\map {\tan^2} {\frac \pi 4 + \frac {a x} 2} } + C
      | c = Tangent is Sine divided by Cosine
}}
{{eqn | r = \frac 1 {2 a \paren {1 - \sin a x} } + \frac 1 {2 a} \ln \size {\map \tan {\frac \pi 4 + \frac {a x} 2} } + C
      | c = Logarithm of Power
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of Sine of a x by 1 plus Cosine of a x

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

Proof:
Let:
{{begin-eqn}}
{{eqn | l = u
      | r = \cos a x
      | c = 
}}
{{eqn | l = \frac {\d u} {\d x}
      | r = -a \sin a x
      | c = Derivative of $\cos a x$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {\sin a x \paren {1 + \cos a x} }
      | r = \int \frac {\sin a x \rd x} {\sin^2 a x \paren {1 + \cos a x} }
      | c = multiplying top and bottom by $\sin a x$
}}
{{eqn | r = \int \frac {\sin a x \rd x} {\paren {1 - \cos^2 a x} \paren {1 + \cos a x} }
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \frac {-1} a \int \frac {\d u} {\paren {1 - u^2} \paren {1 + u} }
      | c = Integration by Substitution
}}
{{eqn | r = \frac {-1} a \int \frac {\d u} {\paren {1 - u} \paren {1 + u}^2}
      | c = Difference of Two Squares
}}
{{eqn | r = \frac {-1} a \paren {\frac 1 {-2} \paren {\frac 1 {1 + u} + \frac {-1} {-2} \ln \size {\frac {1 - u} {1 + u} } } } + C
      | c = Primitive of $\dfrac 1 {\paren {a x + b}^2 \paren {p x + q} }$
}}
{{eqn | r = \frac 1 {2 a \paren {1 + u} } + \frac 1 {4 a} \ln \size {\frac {1 - u} {1 + u} } + C
      | c = simplifying
}}
{{eqn | r = \frac 1 {2 a \paren {1 + \cos a x} } + \frac 1 {4 a} \ln \size {\frac {1 - \cos a x} {1 + \cos a x} } + C
      | c = substituting for $u$
}}
{{eqn | r = \frac 1 {2 a \paren {1 + \cos a x} } + \frac 1 {4 a} \ln \size {\frac {\frac 1 2 \sec^2 \frac {a x} 2} {\frac 1 2 \csc^2 \frac {a x} 2} } + C
      | c = Reciprocal of $1 - \cos$ and Reciprocal of $1 + \cos$
}}
{{eqn | r = \frac 1 {2 a \paren {1 + \cos a x} } + \frac 1 {4 a} \ln \size {\frac {\sin^2 \frac {a x} 2} {\cos^2 \frac {a x} 2} } + C
      | c = Secant is Reciprocal of Cosine
}}
{{eqn | r = \frac 1 {2 a \paren {1 + \cos a x} } + \frac 1 {4 a} \ln \size {\tan^2 \frac {a x} 2} + C
      | c = Tangent is Sine divided by Cosine
}}
{{eqn | r = \frac 1 {2 a \paren {1 + \cos a x} } + \frac 1 {2 a} \ln \size {\tan \frac {a x} 2} + C
      | c = Logarithm of Power
}}
{{end-eqn}}
{{qed}}