avewright/proofwiki-math huggingface dataset:
Theorem: Primitive of Square of Cosecant of a x

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

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

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

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {\sin^2 a x}
      | r = \int \csc^2 a x \rd x
      | c = {{Defof|Cosecant|subdef = Analysis}}
}}
{{eqn | r = \frac {-\cot a x} a + C
      | c = Primitive of $\csc^2 a x$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of Cube of Sine of a x

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

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {\sin^3 a x}
      | r = \int \csc^3 a x \rd x
      | c = Cosecant is $\dfrac 1 \sin$
}}
{{eqn | r = \frac{-\csc a x \cot a x} {2 a} + \frac 1 2 \int \csc a x \rd x
      | c = Primitive of $\csc^n a x$
}}
{{eqn | r = \frac {-\cos a x} {2 a \sin^2 a x} + \frac 1 2 \int \csc a x \rd x
      | c = Cosecant is $\dfrac 1 \sin$ and Cotangent is $\dfrac \cos \sin$
}}
{{eqn | r = \frac {-\cos a x} {2 a \sin^2 a x} + \frac 1 {2 a} \ln \size {\tan \frac {a x} 2} + C
      | c = Primitive of $\csc a x$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Sine of a x by Sine of b x

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

Proof:
{{begin-eqn}}
{{eqn | l = \int \sin a x \sin 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 Sine by Sine
}}
{{eqn | r = \frac 1 2 \int \map \cos {a - b} x \rd x - \frac 1 2 \int \map \cos {a + b} x \rd x
      | c = Linear Combination of Primitives
}}
{{eqn | r = \frac 1 2 \frac {\map \sin {a - b} x} {a - b} - \frac 1 2 \frac {\map \sin {a + b} x} {a + b} + C
      | c = Primitive of $\cos a x$
}}
{{eqn | r = \frac {\map \sin {a - b} x} {2 \paren {a - b} } - \frac {\map \sin {a + b} x} {2 \paren {a + b} } + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of 1 minus Sine of a x

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

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {1 - \sin a x}
      | r = \int \map {\sec^2} {\frac \pi 4 + \frac {a x} 2} \rd x
      | c = Reciprocal of One Minus Sine
}}
{{eqn | n = 1
      | r = \frac 1 2 \int \map {\sec^2} {\frac \pi 4 + \frac {a x} 2} \rd x
      | c = Primitive of Constant Multiple of Function
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = z
      | r = \frac \pi 4 + \frac {a x} 2
}}
{{eqn | l = \frac {\d z} {\d x}
      | r = \frac a 2
      | c = Derivative of Power
}}
{{eqn | ll= \leadsto
      | l = \int \frac {\d x} {1 - \sin a x}
      | r = \frac 1 2 \int \frac 2 a \sec^2 z \rd z
      | c = Integration by Substitution from $(1)$
}}
{{eqn | r = \frac 1 2 \frac 2 a \tan z + C
      | c = Primitive of Square of Secant Function
}}
{{eqn | r = \frac 1 a \map \tan {\frac \pi 4 + \frac {a x} 2} + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of x over 1 minus Sine of a x

:$\ds \int \frac {x \rd x} {1 - \sin a x} = \frac x a \map \tan {\frac \pi 4 + \frac {a x} 2} + \frac 2 {a^2} \ln \size {\map \sin {\frac \pi 4 - \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 = Derivative of Identity Function
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = \frac 1 {1 - \sin a x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac 1 a \map \tan {\frac \pi 4 + \frac {a x} 2}
      | c = Primitive of Reciprocal of 1 minus Sine of a x
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \frac {x \rd x} {1 - \sin a x}
      | r = x \paren {\frac 1 a \map \tan {\frac \pi 4 + \frac {a x} 2} } - \int \paren {\frac 1 a \map \tan {\frac \pi 4 + \frac {a x} 2} } \times 1 \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = \frac x a \map \tan {\frac \pi 4 + \frac {a x} 2} - \frac 1 a \int \map \tan {\frac \pi 4 + \frac {a x} 2} \rd x + C
      | c = simplifying
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = z
      | r = \frac \pi 4 + \frac {a x} 2
}}
{{eqn | l = \frac {\d z} {\d x}
      | r = \frac a 2
      | c = Derivative of Power
}}
{{eqn | ll= \leadsto
      | l = \frac 1 a \int \map \tan {\frac \pi 4 + \frac {a x} 2} \rd x
      | r = \frac 1 a \int \frac 2 a \tan z \rd z
      | c = Integration by Substitution
}}
{{eqn | r = -\frac 2 {a^2} \ln \size {\cos z} + C
      | c = Primitive of $\tan z$: Cosine Form
}}
{{eqn | r = -\frac 2 {a^2} \ln \size {\map \cos {\frac \pi 4 + \frac {a x} 2} } + C
      | c = substituting back for $z$
}}
{{eqn | r = -\frac 2 {a^2} \ln \size {\map \sin {\frac \pi 2 - \paren {\frac \pi 4 + \frac {a x} 2} } } + C
      | c = Sine of Complement equals Cosine
}}
{{eqn | r = -\frac 2 {a^2} \ln \size {\map \sin {\frac \pi 4 - \frac {a x} 2} } + C
      | c = 
}}
{{end-eqn}}
Putting it all together:
:$\ds \int \frac {x \rd x} {1 - \sin a x} = \frac x a \map \tan {\frac \pi 4 + \frac {a x} 2} + \frac 2 {a^2} \ln \size {\map \sin {\frac \pi 4 - \frac {a x} 2} } + C$
{{qed}}
Theorem: Primitive of Reciprocal of 1 plus Sine of a x

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

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {1 + \sin a x}
      | r = \int \frac 1 2 \map {\sec^2} {\frac \pi 4 - \frac {a x} 2} \rd x
      | c = Reciprocal of One Plus Sine
}}
{{eqn | n = 1
      | r = \frac 1 2 \int \map {\sec^2} {\frac \pi 4 - \frac {a x} 2} \rd x
      | c = Primitive of Constant Multiple of Function
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = z
      | r = \frac \pi 4 - \frac {a x} 2
}}
{{eqn | l = \frac {\d z} {\d x}
      | r = -\frac a 2
      | c = Derivative of Power
}}
{{eqn | ll= \leadsto
      | l = \int \frac {\d x} {1 + \sin a x}
      | r = -\frac 1 2 \int \frac 2 a \sec^2 z \rd z
      | c = Integration by Substitution from $(1)$
}}
{{eqn | r = -\frac 1 2 \cdot \frac 2 a \tan z + C
      | c = Primitive of Square of Secant Function
}}
{{eqn | r = -\frac 1 a \map \tan {\frac \pi 4 - \frac {a x} 2} + C
      | c = substituting for $z$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of x over 1 plus Sine of a x

:$\ds \int \frac {x \rd x} {1 + \sin a x} = -\frac x a \map \tan {\frac \pi 4 - \frac {a x} 2} + \frac 2 {a^2} \ln \size {\map \sin {\frac \pi 4 + \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 = Derivative of Identity Function
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = \frac 1 {1 + \sin a x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = -\frac 1 a \map \tan {\frac \pi 4 - \frac {a x} 2}
      | c = Primitive of $\dfrac 1 {1 + \sin a x}$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \frac {x \rd x} {1 + \sin a x}
      | r = x \paren {-\frac 1 a \map \tan {\frac \pi 4 - \frac {a x} 2} } - \int \paren {-\frac 1 a \map \tan {\frac \pi 4 - \frac {a x} 2} } \times 1 \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = -\frac x a \map \tan {\frac \pi 4 - \frac {a x} 2} + \frac 1 a \int \map \tan {\frac \pi 4 - \frac {a x} 2} \rd x + C
      | c = simplifying
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = z
      | r = \frac \pi 4 - \frac {a x} 2
}}
{{eqn | l = \frac {\d z} {\d x}
      | r = -\frac a 2
      | c = Derivative of Power
}}
{{eqn | ll= \leadsto
      | l = \frac 1 a \int \map \tan {\frac \pi 4 - \frac {a x} 2} \rd x
      | r = -\frac 1 a \int \frac 2 a \tan z \rd z
      | c = Integration by Substitution
}}
{{eqn | r = -\frac {-2} {a^2} \ln \size {\cos z} + C
      | c = Primitive of $\tan z$: Cosine Form
}}
{{eqn | r = \frac 2 {a^2} \ln \size {\map \cos {\frac \pi 4 - \frac {a x} 2} } + C
      | c = substituting back for $z$
}}
{{eqn | r = \frac 2 {a^2} \ln \size {\map \sin {\frac \pi 2 - \paren {\frac \pi 4 - \frac {a x} 2} } } + C
      | c = Sine of Complement equals Cosine
}}
{{eqn | r = \frac 2 {a^2} \ln \size {\map \sin {\frac \pi 4 + \frac {a x} 2} } + C
      | c = 
}}
{{end-eqn}}
Putting it all together:
:$\ds \int \frac {x \rd x} {1 - \sin a x} = -\frac x a \map \tan {\frac \pi 4 - \frac {a x} 2} + \frac 2 {a^2} \ln \size {\map \sin {\frac \pi 4 + \frac {a x} 2} } + C$
{{qed}}
Theorem: Primitive of Reciprocal of Square of 1 minus 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} {\frac \pi 4 + \frac {a x} 2} }^2 \rd x
      | c = Reciprocal of One Minus 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: Reciprocal of One Minus Sine

:$\dfrac 1 {1 - \sin x} = \dfrac 1 2 \map {\sec^2} {\dfrac \pi 4 + \dfrac x 2}$

Proof:
{{begin-eqn}}
{{eqn | l = 1 - \sin x
      | r = \sin \frac \pi 2 - \sin x
      | c = Sine of Right Angle
}}
{{eqn | r = 2 \map \cos {\frac 1 2 \paren {\frac \pi 2 + x} } \map \sin {\frac 1 2 \paren {\frac \pi 2 - x} }
      | c = Sine minus Sine
}}
{{eqn | r = 2 \map \cos {\frac \pi 4 + \frac x 2} \map \sin {\frac \pi 4 - \frac x 2}
      | c = simplifying
}}
{{eqn | r = 2 \map \cos {\frac \pi 4 + \frac x 2} \map \cos {\frac \pi 2 - \paren {\frac \pi 4 - \frac x 2} }
      | c = Cosine of Complement equals Sine
}}
{{eqn | r = 2 \map \cos {\frac \pi 4 + \frac x 2} \map \cos {\frac \pi 4 + \frac x 2}
      | c = simplifying
}}
{{eqn | r = 2 \map {\cos^2} {\frac \pi 4 + \frac x 2}
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \frac 1 {1 - \sin x}
      | r = \frac 1 2 \map {\sec^2} {\frac \pi 4 + \frac x 2}
      | c = {{Defof|Secant Function}}
}}
{{end-eqn}}
{{qed}}
Theorem: Reciprocal of One Plus Sine

:$\dfrac 1 {1 + \sin x} = \dfrac 1 2 \map {\sec^2} {\dfrac \pi 4 - \dfrac x 2}$

Proof:
{{begin-eqn}}
{{eqn | l = 1 + \sin x
      | r = \sin \frac \pi 2 + \sin x
      | c = Sine of Right Angle
}}
{{eqn | r = 2 \map \sin {\frac 1 2 \paren {\frac \pi 2 + x} } \map \cos {\frac 1 2 \paren {\frac \pi 2 - x} }
      | c = Sine minus Sine
}}
{{eqn | r = 2 \map \sin {\frac \pi 4 + \frac x 2} \map \cos {\frac \pi 4 - \frac x 2}
      | c = simplifying
}}
{{eqn | r = 2 \map \cos {\frac \pi 2 - \paren {\frac \pi 4 - \frac x 2} } \map \cos {\frac \pi 4 - \frac x 2}
      | c = Cosine of Complement equals Sine
}}
{{eqn | r = 2 \map \cos {\frac \pi 4 - \frac x 2} \map \cos {\frac \pi 4 - \frac x 2}
      | c = simplifying
}}
{{eqn | r = 2 \map {\cos^2} {\frac \pi 4 - \frac x 2}
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \frac 1 {1 + \sin x}
      | r = \frac 1 2 \map {\sec^2} {\frac \pi 4 - \frac x 2}
      | c = {{Defof|Secant Function}}
}}
{{end-eqn}}
{{qed}}
Theorem: Power Series Expansion for Cosecant Function

The cosecant function has a Laurent series expansion:
{{begin-eqn}}
{{eqn | l = \csc x
      | r = \sum_{n \mathop = 0}^\infty \dfrac {\paren {-1}^{n - 1} 2 \paren {2^{2 n - 1} - 1} B_{2 n} \, x^{2 n - 1} } {\paren {2 n}!}
      | c = 
}}
{{eqn | r = \frac 1 x + \frac x 6 + \frac {7 x^3} {360} + \frac {31 x^5} {15 \, 120} + \cdots
      | c = 
}}
{{end-eqn}}
where $B_n$ denotes the Bernoulli numbers.
This converges for $0 < \size x < \pi$.

Proof:
{{begin-eqn}}
{{eqn | l = \sin x
      | r = 2 \sin \dfrac x 2 \cos \dfrac x 2
      | c = Double Angle Formula for Sine
}}
{{eqn | ll= \leadstoandfrom
      | l = \dfrac 1 {\sin x}
      | r = \dfrac 1 {2 \sin \dfrac x 2 \cos \dfrac x 2}
      | c = taking the reciprocal of both sides
}}
{{eqn | ll= \leadstoandfrom
      | l = \csc x
      | r = \dfrac 1 2 \csc \dfrac x 2 \sec \dfrac x 2
      | c = Cosecant is Reciprocal of Sine, Secant is Reciprocal of Cosine
}}
{{eqn | r = \dfrac 1 2 \csc \dfrac x 2 \dfrac 2 {e^{i \frac x 2} + e^{-i \frac x 2} }
      | c = Euler's Secant Identity
}}
{{eqn | r = \csc \dfrac x 2 \dfrac {e^{-i \frac x 2} } {1 + e^{-i x} }
}}
{{eqn | ll= \leadstoandfrom
      | l = \csc x \paren {1 + e^{-i x} }
      | r = \csc \dfrac x 2 e^{-i \frac x 2}
      | c = multiplying both sides by $1 + e^{-i x}$
}}
{{eqn | ll= \leadstoandfrom
      | l = \csc x
      | r = \csc \dfrac x 2 e^{-i \frac x 2} - \csc x e^{-i x}
      | c = subtracting $\csc x e^{-i x}$ from both sides
}}
{{eqn | r = \dfrac {2 i} {e^{i \frac x 2} - e^{-i \frac x 2} } e^{-i \frac x 2} - \dfrac {2 i} {e^{i x} - e^{-i x} } e^{-i x}
      | c = Euler's Cosecant Identity
}}
{{eqn | r = 2 \dfrac i {e^{i x} - 1} - \dfrac {2 i} {e^{2 i x} - 1}
}}
{{eqn | r = \dfrac 1 x \paren {2 \dfrac {i x} {e^{i x} - 1} - \dfrac {2 i x} {e^{2 i x} - 1} }
}}
{{eqn | r = \dfrac 1 x \sum_{n \mathop = 0}^\infty \paren {2 \dfrac {\paren {i x}^n B_n} {n!} - \dfrac {\paren {2 i x}^n B_n} {n!} }
      | c = {{Defof|Bernoulli Numbers}}
}}
{{eqn | r = \dfrac 1 x \sum_{n \mathop = 0}^\infty \dfrac {B_n \paren {2 \paren {i x}^n - \paren {2 i x}^n} } {n!}
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \dfrac {B_n i^n x^{n - 1} 2 \paren {1 - 2^{n - 1} } } {n!}
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \dfrac {B_{2 n} i^{2 n} x^{2 n - 1} 2 \paren {1 - 2^{2 n - 1} } } {\paren {2 n}!}
      | c = Odd Bernoulli Numbers Vanish and the term $n = 1$ vanishes
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \dfrac {B_{2 n} \paren {-1}^{n - 1} x^{2 n - 1} 2 \paren {2^{2 n - 1} - 1} } {\paren {2 n}!}
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: Periodic Function plus Constant

Let $f: \R \to \R$ be a real function.
Let $k \in \R$ be constant.
Then $f$ is periodic with period $L$ {{iff}} $f + k$ is periodic with period $L$.

Proof:
=== Sufficient Condition ===
Let $f$ be periodic with period $L$.
Then:
{{begin-eqn}}
{{eqn | l = \map f x
      | r = \map f {x + L}
      | c = {{Defof|Periodic Real Function}}
}}
{{eqn | ll= \leadsto
      | l = \map f x + k
      | r = \map f {x + L} + k
}}
{{end-eqn}}
Thus $f + k$ has been shown to be periodic with period $L$.
{{qed|lemma}}
Theorem: Derivative of Periodic Real Function

Let $f: \R \to \R$ be a real function.
Let $f$ be differentiable on all of $\R$.
Let $f$ be periodic with period $L$.
Then its derivative is also periodic with period $L$.

Proof:
Let $f$ be differentiable on all of $\R$.
Let $f$ be periodic with period $L$.
Then taking the derivative of both sides using the Chain Rule for Derivatives yields:
:$\map f x = \map f {x + L} \implies \map {f'} x = \map {f'} {x + L}$
Let $L'$ be the period of $f'$.
$f$ is differentiable and therefore continuous, by Differentiable Function is Continuous.
From Image of Closed Real Interval is Bounded, it follows that $f$ is bounded on $\closedint 0 {\size L}$.
But from the General Periodicity Property, it follows that $f$ is bounded on all of $\R$.
Then from Primitive of Periodic Real Function, it follows that $L'$ is the period of $f$.
But we had previously established that $L$ was the period of $f$.
Hence it follows that $L' = L$.
Hence the result.
{{qed}}
Theorem: Sum of Two Odd Powers/Examples/Sum of Two Cubes

:$x^3 + y^3 = \paren {x + y} \paren {x^2 - x y + y^2}$

Proof:
From Difference of Two Powers:
:$\ds a^n - b^n = \paren {a - b} \sum_{j \mathop = 0}^{n - 1} a^{n - j - 1} b^j$
Let $x = a$ and $y = -b$.
Then:
{{begin-eqn}}
{{eqn | l = x^3 + y^3
      | r = x^3 - \paren {-y^3}
      | c = 
}}
{{eqn | r = x^3 - \paren {-y}^3
      | c = 
}}
{{eqn | r = \paren {x - \paren {-y} } \sum_{j \mathop = 0}^2 x^{n - j - 1} \paren {-y}^j
      | c = 
}}
{{eqn | r = \paren {x + y} \paren {x^2 + x \paren {-y} + \paren {-y}^2}
      | c = 
}}
{{eqn | r = \paren {x + y} \paren {x^2 - x y + y^2}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Two Odd Powers/Examples/Sum of Two Cubes

:$x^3 + y^3 = \paren {x + y} \paren {x^2 - x y + y^2}$

Proof:
From Sum of Two Odd Powers:
:$a^{2 n + 1} + b^{2 n + 1} = \paren {a + b} \paren {a^{2 n} - a^{2 n - 1} b + a^{2 n - 2} b^2 - \dotsb + a b^{2 n - 1} + b^{2 n} }$
We have that $3 = 2 \times 1 + 1$.
Hence setting $n = 1$ gives the result.
{{qed}}
Theorem: Primitive of Periodic Real Function

Let $f: \R \to \R$ be a real function.
Let $F$ be a primitive of $f$ that is bounded on all of $\R$.
Let $f$ be periodic with period $L$.
Then $F$ is also periodic with period $L$.

Proof:
{{MissingLinks}}
Let $f$ be periodic with period $L$.
Let $f$ have a primitive $F$ that is bounded on all of $\R$.
By definition of a periodic function, it is seen that:
:$\map f x = \map f {x + L}$.
Then:
:$\ds \int \map f x \rd x$
and:
:$\ds \int \map f {x + L} \rd x$
are both primitives of the same function.
So by Primitives which Differ by Constant:
{{begin-eqn}}
{{eqn | l = \int \map f x \rd x + C
      | r = \int \map f {x + L} \rd x
}}
{{eqn | r = \int \map f {x + L} \frac {\map \d {x + L} } {\d x} \rd x
      | c = as $\dfrac {\map \d {x + L} } {\d x} = 1$
}}
{{eqn | r = \int \map f {x + L} \map \d {x + L}
      | c = Integration by Substitution
}}
{{eqn | ll= \leadsto
      | l = \map F x + C
      | r = \map F {x + L}
}}
{{end-eqn}}
{{AimForCont}} $C \ne 0$.
Then it is to be shown that for all $k \in \N_{> 0}$:
:$\map F x + k C = \map F {x + k L}$
The case for $k = 1$ has already been proven, so this will be proven by induction.
Suppose that for some $n \in \N_{> 0}$ we have:
:$\map F x + n C = \map F {x + n L}$
Then
{{begin-eqn}}
{{eqn | l = \map F {x + \paren {n + 1} L}
      | r = \map F {x + L + n L}
}}
{{eqn | r = \map F {x + L} + n C
      | c = by the induction hypothesis
}}
{{eqn | r = \map F x + \paren {n + 1} C
      | c = by the base case
}}
{{end-eqn}}
{{qed|lemma}}
Holding $x$ fixed yields:
:$\ds \lim_{k \mathop \to \infty} \size {\map F {x + k L} } = \lim_{k \mathop \to \infty} \size {\map F x + k C} = \infty$
and so $\map F x$ is unbounded.
But we had previously established that $\map F x$ was bounded.
This is a contradiction.
Therefore our assumption that $C \ne 0$ was false.
Hence $C = 0$ and so:
:$\map F x = \map F {x + L}$
It has been shown that $F$ is periodic.
{{qed|lemma}}
Let $L'$ be the period of $F$.
Then:
{{begin-eqn}}
{{eqn | l = \map F x
      | r = \map F {x + L'}
}}
{{eqn | ll= \leadsto
      | l = \map {F'} x
      | r = \map {F'} {x + L'}
      | c = Chain Rule for Derivatives
}}
{{eqn | ll= \leadsto
      | l = \map f x
      | r = \map f {x + L'}
      | c = {{Defof|Primitive of Real Function}}
}}
{{end-eqn}}
But it was previously established that $L$ was the period of $f$.
Hence it follows that $L' = L$.
Hence the result.
{{qed}}
Theorem: Primitive of Reciprocal of x squared by x cubed plus a cubed/Lemma

:$\ds \int \frac {\d x} {x^2 \paren {x^3 + a^3} } = \frac {-1} {a^3 x} - \frac 1 {a^3} \int \frac {x \rd x} {\paren {x^3 + a^3} }$

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {x^2 \paren {x^3 + a^3} }
      | r = \int \frac {a^3 \rd x} {a^3 x^2 \paren {x^3 + a^3} }
      | c = multiplying top and bottom by $a^3$
}}
{{eqn | r = \int \frac {\paren {x^3 + a^3 - x^3} \rd x} {a^3 x^2 \paren {x^3 + a^3} }
      | c = 
}}
{{eqn | r = \frac 1 {a^3} \int \frac {\paren {x^3 + a^3} \rd x} {x^2 \paren {x^3 + a^3} } - \frac 1 {a^3} \int \frac {x^3 \rd x} {x^2 \paren {x^3 + a^3} }
      | c = Linear Combination of Primitives
}}
{{eqn | r = \frac 1 {a^3} \int \frac {\d x} {x^2} - \frac 1 {a^3} \int \frac {x \rd x} {\paren {x^3 + a^3} }
      | c = simplifying
}}
{{eqn | r = \frac 1 {a^3} \paren {\frac {-1} x} - \frac 1 {a^3} \int \frac {x \rd x} {\paren {x^3 + a^3} }
      | c = Primitive of Power
}}
{{eqn | r = \frac {-1} {a^3 x} - \frac 1 {a^3} \int \frac {x \rd x} {\paren {x^3 + a^3} }
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Category:Primitives involving x cubed plus a cubed/Lemmata
Category:Primitive of Reciprocal of x squared by x cubed plus a cubed
mdcpwwrwwmbfu7ewomkk9o6cexu7g6g
Theorem: Sum of Two Fourth Powers

:$x^4 + y^4 = \paren {x^2 + \sqrt 2 x y + y^2} \paren {x^2 - \sqrt 2 x y + y^2}$

Proof:
{{begin-eqn}}
{{eqn | r = \paren {x^2 + \sqrt 2 x y + y^2} \paren {x^2 - \sqrt 2 x y + y^2}
      | o = 
      | c = 
}}
{{eqn | r = x^2 \paren {x^2 - \sqrt 2 x y + y^2} + \sqrt 2 x y \paren {x^2 - \sqrt 2 x y + y^2} + y^2 \paren {x^2 - \sqrt 2 x y + y^2}
      | c = 
}}
{{eqn | r = x^4 - \sqrt 2 x^3 y + x^2 y^2 + \sqrt 2 x^3 y - 2 x^2 y^2 + \sqrt 2 x y^3 + x^2 y^2 - \sqrt 2 x y^3 + y^4
      | c = 
}}
{{eqn | r = x^4 + y^4
      | c = gathering terms
}}
{{end-eqn}}
{{qed}}
Category:Fourth Powers
sq6h9z4jtye8065i0t206pf88iyksej
Theorem: Pumping Lemma for Regular Languages

Let $\LL_3$ be the set of regular languages.
{{explain|Is it a set? Does this need to be proved? Intuition would suggest that it would be a class.}}
Then the following holds:
$\forall L \in \LL_3: \exists n_0 \in \N_0: \forall z \in L: \card z > n_0 \implies \exists u, v, w$ such that:
:$z = u \cdot v \cdot w$
:$\card v > 0$
:$\card {u v} < n_0$
:$\forall i \in \N_0: u \cdot v^i \cdot w \in L$

Proof:
=== For finite languages ===
For any ''finite'' regular language $L_{fin}$, the proof is simple.
Let $s_{maxlen} \in L_{fin}$.
Thus:
:$\forall s \in L_{fin}: \card s \le \card {s_{maxlen} }$
Now choose $n_0 > \card {s_{maxlen} }$.
The implication now trivially holds because the premise:
:$\paren {\card z > n_0}$
is false.
{{qed|lemma}}