avewright/proofwiki-math huggingface dataset:
Theorem: Power Rule for Derivatives

Let $n \in \R$.
Let $f: \R \to \R$ be the real function defined as $\map f x = x^n$.
Then:
:$\map {f'} x = n x^{n - 1}$
everywhere that $\map f x = x^n$ is defined.
When $x = 0$ and $n = 0$, $\map {f'} x$ is undefined.

Proof:
We are going to prove that $\map {f'} x = n x^{n - 1}$ holds for all real $n$.
To do this, we compute the limit $\ds \lim_{h \mathop \to 0} \frac {\paren {x + h}^n - x^n} h$:
{{begin-eqn}}
{{eqn | l = \frac {\paren {x + h}^n - x^n} h
      | r = \frac {x^n} h \paren {\paren {1 + \frac h x}^n - 1}
      | c = 
}}
{{eqn | r = \frac{x^n} h \paren {e^{n \map \ln {1 + \frac h x} } - 1}
      | c = 
}}
{{eqn | r = x^n \cdot \frac {e^{n \map \ln {1 + \frac h x} } - 1} {n \map \ln {1 + \frac h x} } \cdot \frac {n \map \ln {1 + \frac h x} } {\frac h x} \cdot \frac 1 x
      | c = 
}}
{{end-eqn}}
Now we use the following results:
:$\ds \lim_{x \mathop \to 0} \frac {\exp x - 1} x = 1$ from Derivative of Exponential at Zero
:$\ds \lim_{x \mathop \to 0} \frac {\map \ln {1 + x} } x = 1$ from Derivative of Logarithm at One
to obtain:
:$x^n \cdot \dfrac {e^{n \map \ln {1 + \frac h x} } - 1} {n \map \ln {1 + \dfrac h x} } \cdot \dfrac {n \map \ln {1 + \dfrac h x}} {\dfrac h x} \cdot \dfrac 1 x \to n x^{n - 1}$ as $h \to 0$
Hence the result.
{{qed}}
Theorem: Power Rule for Derivatives

Let $n \in \R$.
Let $f: \R \to \R$ be the real function defined as $\map f x = x^n$.
Then:
:$\map {f'} x = n x^{n - 1}$
everywhere that $\map f x = x^n$ is defined.
When $x = 0$ and $n = 0$, $\map {f'} x$ is undefined.

Proof:
Note this proof does not hold for $x = 0$.
Let $y$ = $\map f x$.
Then $y = x^n$.
Then:
{{begin-eqn}}
{{eqn | l = y
      | r = x^n
}}
{{eqn | ll= \leadsto
      | l = \size y
      | r = \size {x^n}
      | c = taking the absolute value of both sides
}}
{{eqn | r = \size x^n
      | c = Absolute Value of Power
}}
{{eqn | ll= \leadsto
      | l = \ln \size y
      | r = \map \ln {\size x^n}
      | c = taking the natural logarithm of both sides
}}
{{eqn | r = n \ln \size x
      | c = Logarithm of Power
}}
{{end-eqn}}
Using:
* Derivative of Composite Function
* Derivative of Constant Multiple
* {{Corollary|Primitive of Reciprocal|2}}
and taking the derivative of both sides with respect to $x$ gives:
:$\dfrac 1 y \dfrac {\d y} {\d x} = n \dfrac 1 x$
Multiplying both sides of the equation by $y$ yields:
:$\dfrac {\d y} {\d x} = n \dfrac y x$
Substituting $x^n$ for $y$:
:$\dfrac {\d y} {\d x} = n \dfrac {x^n} x$
From Quotient of Powers:
:$\dfrac {\d y} {\d x} = n x^{n - 1}$
{{qed}}
Theorem: Basel Problem

:$\ds \map \zeta 2 = \sum_{n \mathop = 1}^\infty {\frac 1 {n^2} } = \frac {\pi^2} 6$
where $\zeta$ denotes the Riemann zeta function.

Proof:
By Riemann Zeta Function as a Multiple Integral, 
:$\ds \map \zeta 2 = \int_0^1 \int_0^1 \frac 1 {1 - x y} \rd x\rd y$ 
Let $\tuple {u, v} = \tuple {\dfrac {x + y} 2, \dfrac{y - x} 2}$ so that:
:$\tuple {x, y} = \tuple {u - v, u + v}$
The Jacobian is:
:$\size J = \size {\dfrac {\partial \tuple {x, y} } {\partial \tuple {u, v} } } = 2$
Then, by Change of Variables Theorem (Multivariable Calculus):
:$\map \zeta 2 = \ds 2 \iint \limits_S \frac {\d u \rd v} {1 - u^2 + v^2}$
where $S$ is the square defined by the coordinates:
:$\tuple {0, 0}, \ \tuple {\dfrac 1 2, -\dfrac 1 2}, \ \tuple {1, 0}, \ \tuple {\dfrac 1 2, \dfrac 1 2}$
Exploiting the symmetry of the square and the function over the $u$-axis, we have:
:$\map \zeta 2 = \ds 4 \paren {\int_0^{\frac 1 2} \! \int_0^u \frac {\d v \rd u} {1 - u^2 + v^2} + \int_{\frac 1 2}^1 \! \int_0^{1 - u} \frac {\d v \rd u} {1 - u^2 + v^2} }$
Factoring $1 - u^2$ gives us:
:$\map \zeta 2 = \ds 4 \paren {\int_0^{\frac 1 2} \! \int_0^u \frac 1 {1 - u^2} \frac {\d v \rd u} {\frac {v^2} {1 - u^2} + 1} + \int_{\frac 1 2}^1 \! \int_0^{1 - u} \frac 1 {1 - u^2} \frac {\d v \rd u} {\frac {v^2} {1 - u^2} + 1} }$
and letting:
:$s = \dfrac v {\sqrt {1 - u^2} }, \rd s = \dfrac 1 {\sqrt {1 - u^2} }$
allows us to make a substitution into each integral, giving:
:$\map \zeta 2 = \ds 4 \paren {\int_0^{\frac 1 2} \frac 1 {\sqrt {1 - u^2} } \map \arctan {\frac u {\sqrt {1 - u^2} } } \rd u + \int_{\frac 1 2}^1 \frac 1 {\sqrt {1 - u^2} } \map \arctan {\frac {1 - u} {\sqrt {1 - u^2} } } \rd u}$
Consider the right triangle with sides $1$, $x$ and $\sqrt {1 - x^2}$.
Applying Pythagoras's Theorem:
:$\arcsin x = \arctan \dfrac x {\sqrt {1 - x^2} }$
Let:
{{begin-eqn}}
{{eqn | l = \theta
      | r = \map \arctan {\dfrac{1 - u} {\sqrt{1 - u^2} } }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \tan^2 \theta
      | r = \frac {1 - u} {1 + u}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sec^2 \theta
      | r = \frac 2 {1 + u}
      | c = Difference of Squares of Secant and Tangent
}}
{{eqn | ll= \leadsto
      | l = \cos 2 \theta
      | r = u
      | c = {{Corollary|Double Angle Formula for Cosine|1}}
}}
{{eqn | ll= \leadsto
      | l = \theta
      | r = \dfrac 1 2 \arccos u
      | c = taking arccosines of both sides
}}
{{eqn | r = \frac \pi 4 - \frac {\arcsin u} 2
      | c = Sine of Complement equals Cosine
}}
{{end-eqn}}
This allows us to convert the arctangents from the integrals into arcsines:
:$\map \zeta 2 = \ds 4 \paren {\int_0^{\frac 1 2} {\frac {\arcsin u} {\sqrt {1 - u^2} } \rd u} + \int_{\frac 1 2}^1 {\frac 1 {\sqrt {1 - u^2} } \paren {\frac \pi 4 - \frac {\arcsin u} 2} \rd u} }$
Substituting:
:$s = \arcsin u$, $\rd s = \dfrac 1 {\sqrt{1 - u^2} }$
into the arcsines, and splitting the second integral:
:$\map \zeta 2 = 4 \paren {\dfrac {\pi^2} {72} + \dfrac {\pi^2} {36} } = \dfrac {\pi^2} 6$
{{qed}}
Theorem: Basel Problem

:$\ds \map \zeta 2 = \sum_{n \mathop = 1}^\infty {\frac 1 {n^2} } = \frac {\pi^2} 6$
where $\zeta$ denotes the Riemann zeta function.

Proof:
Let:
:$\ds P_k = x \prod_{n \mathop = 1}^k \paren {1 - \frac {x^2} {n^2 \pi^2} }$
We note that:
{{begin-eqn}}
{{eqn | l = P_k - P_{k - 1}
      | r = \paren {-\frac {x^3} {k^2 \pi^2} } \prod_{n \mathop = 1}^{k - 1} \paren {1 - \frac {x^2} {n^2 \pi^2} }
      | c = 
}}
{{eqn | r = -\frac {x^3} {k^2 \pi ^2} + \map O {x^5}
      | c = {{Defof|Big-O Notation}}
}}
{{end-eqn}}
By Telescoping Series we find that the coefficient of $x^3$ in $P_k$ is given by:
:$(1): \quad \ds -\frac 1 {\pi^2} \sum_{n \mathop = 1}^k \frac 1 {n^2}$
We also have the following two representations of the Sine of x:
{{begin-eqn}}
{{eqn | l = \sin x
      | r = x \prod_{n \mathop = 1}^\infty \paren {1 - \dfrac {x^2} {n^2 \pi^2} }
      | c = Euler Formula for Sine Function
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \sin x
      | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \dfrac {x^{2 n + 1} } {\paren {2 n + 1}!} = x - \dfrac {x^3} {3!} + \dfrac {x^5} {5!} - \dfrac {x^7} {7!} + \cdots
      | c = Power Series Expansion for Sine Function
}}
{{end-eqn}}
So by taking the limit as $k \to \infty$ in $(1)$ and equating with the coefficient of $x^3$ in the Power Series Expansion for Sine Function, we can deduce:
:$\ds -\frac 1 {\pi^2} \sum_{n \mathop = 1}^\infty \frac 1 {n^2} = -\frac 1 {3!}$
hence:
:$\ds \sum_{n \mathop = 1}^{\infty} \frac 1 {n^2} = \frac {\pi^2} 6$
{{qed}}
Theorem: Basel Problem

:$\ds \map \zeta 2 = \sum_{n \mathop = 1}^\infty {\frac 1 {n^2} } = \frac {\pi^2} 6$
where $\zeta$ denotes the Riemann zeta function.

Proof:
Let $x \in \openint 0 {\dfrac \pi 2}$ and let $n$ be a non-negative integer.
{{begin-eqn}}
{{eqn | l = \frac {\map \cos {2 n + 1} x + i \map \sin {2 n + 1} x} {\sin^{2 n + 1} x} 
      | r = \frac {\paren {\cos x + i \sin x}^{2 n + 1} } {\sin^{2 n + 1} x}
      | c = De Moivre's Formula
}}
{{eqn | r = \paren {\cot x + i}^{2 n + 1}
      | c = 
}}
{{eqn | r = \sum_{r \mathop = 0}^{2 n + 1} \binom {2 n + 1} r i^r \cot^{2 n + 1 - r} x
      | c = Binomial Theorem
}}
{{eqn | ll= \leadsto
      | l = \frac {\map \sin {2 n + 1} x} {\sin^{2 n + 1} x}
      | r = \sum_{r \mathop = 0}^n \binom {2 n + 1} {2 r + 1} \paren {-1}^r \cot^{2 \paren {n - r} } x
      | c = equating imaginary parts
}}
{{end-eqn}}
Let $x_k = \dfrac {k \pi} {2 n + 1}$ for $k = 1, 2, \ldots, n$. 
Then:
:$\sin \paren {2 n + 1} x_k = 0$
So we have:
:$\ds \sum_{r \mathop = 0}^n \binom {2 n + 1} {2 r + 1} \paren {-1}^r \cot^{2 \paren {n - r} } x_k = 0$
for $k = 1, 2, \ldots, n$.
The numbers $x_k$ are all distinct and in the interval $\openint 0 {\dfrac \pi 2}$. 
By Shape of Cotangent Function, $\cot x$ is positive and injective in the interval $\openint 0 {\dfrac \pi 2}$.
Therefore $\cot^2 x$ is also injective in this interval. 
Hence the numbers $c_k = \cot^2 x_k$ are distinct for $k = 1, 2, \ldots, n$. 
These numbers are the $n$ distinct roots of the $n$th degree polynomial:
:$\ds \map f c := \sum_{r \mathop = 0}^n \binom {2 n + 1} {2 r + 1} (-1)^r c^{n - r}$
By Viète's Formulas, we can calculate the sum of the roots:
:$\ds \sum_{k \mathop = 1}^n \cot^2 x_k = \frac {\binom {2 n + 1} 3} {\binom {2 n + 1} 1} = \frac {2 n \paren {2 n - 1} } 6$
From the Difference of Squares of Cosecant and Cotangent $\cot^2 x = \csc^2 x - 1$ we can similarly deduce:
:$\ds \sum_{k \mathop = 1}^n \csc^2 x_k = \frac {2 n \paren {2 n - 1} } 6 + n = \frac {2 n \paren {2 n + 2} } 6$
By Shape of Sine Function, $\sin x$ is positive in the interval $\openint 0 {\dfrac \pi 2}$. 
So from the Tangent Inequality $\sin x < x < \tan x$ for $x \in \openint 0 {\dfrac \pi 2}$, we can deduce that $\cot^2 x < 1 / x^2 < \csc^2 x$ in the same interval.
Summing this inequality from $x_1$ to $x_n$ gives:
{{begin-eqn}}
{{eqn | l = \frac {2 n \paren {2 n - 1} } 6
      | o = <
      | r = \sum_{k \mathop = 1}^n \paren {\frac {2 n + 1} {k \pi} }^2
      | c = 
}}
{{eqn | o = <
      | r = \frac {2 n \paren {2 n + 2} } 6
      | c = 
}}
{{end-eqn}}
or equivalently:
{{begin-eqn}}
{{eqn | l = \frac {\pi^2} 6 \frac {2 n \paren {2 n - 1} } {\paren {2 n + 1}^2}
      | o = <
      | r = \sum_{k \mathop = 1}^n \frac 1 {k^2}
      | c = 
}}
{{eqn | o = <
      | r = \frac {\pi^2} 6 \frac {2 n \paren {2 n + 2} } {\paren {2 n + 1}^2}
      | c = 
}}
{{end-eqn}}
By Combination Theorem for Limits of Real Functions, the {{LHS}} and {{RHS}} both tend to $\dfrac {\pi^2} 6$ as $n$ tends to infinity. 
Therefore by the Squeeze Theorem:
:$\map \zeta 2 = \ds \sum_{k \mathop = 1}^\infty \frac 1 {k^2} = \frac {\pi^2} 6$
{{qed}}
Theorem: Basel Problem

:$\ds \map \zeta 2 = \sum_{n \mathop = 1}^\infty {\frac 1 {n^2} } = \frac {\pi^2} 6$
where $\zeta$ denotes the Riemann zeta function.

Proof:
From Sum of Reciprocals of Squares of Odd Integers:
:$\ds \sum_{n \mathop = 0}^\infty \frac 1 {\paren {2 n + 1}^2} = \frac {\pi^2} 8$
Hence:
{{begin-eqn}}
{{eqn | l = \sum_{n \mathop = 1}^\infty \frac 1 {n^2}
      | r = \sum_{n \mathop = 1}^\infty \frac 1 {\paren {2 n}^2} + \sum_{n \mathop = 0}^\infty \frac 1 {\paren {2 n + 1}^2}
      | c =
}}
{{eqn | r = \frac 1 4 \sum_{n \mathop = 1}^\infty \frac 1 {n^2} + \frac {\pi^2} 8
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sum_{n \mathop = 1}^\infty \frac 1 {n^2}
      | r = \frac {\pi^2} 6
}}
{{end-eqn}}
{{qed}}
Theorem: Basel Problem

:$\ds \map \zeta 2 = \sum_{n \mathop = 1}^\infty {\frac 1 {n^2} } = \frac {\pi^2} 6$
where $\zeta$ denotes the Riemann zeta function.

Proof:
Let the function $f_n$ be defined as:
:$(1): \quad \map {f_n} x := \dfrac 1 2 + \cos x + \cos 2 x + \cdots + \cos n x$
By Lagrange's Cosine Identity:
:$(2): \quad \map {f_n} x = \dfrac {\map \sin {\paren {2 n + 1} x / 2} } {2 \map \sin {x / 2} }$
Let $E_n$ be defined as:
{{begin-eqn}}
{{eqn | l = E_n
      | r = \int_0^\pi x \map {f_n} x \rd x
      | c = 
}}
{{eqn | n = 3
      | r = \frac {\pi^2} 4 + \sum_{k \mathop = 1}^n \paren {\frac {\paren {-1}^k - 1} {k^2} }
      | c = Primitive of $x \cos a x$ and algebra
}}
{{end-eqn}}
{{handwaving|show the algebra - not clear}}
The terms for even $k$ on the {{RHS}} are zero, so:
:$\ds (4): \quad \dfrac 1 2 E_{2 n - 1} = \dfrac {\pi^2} 8 - \sum_{k \mathop = 1}^n \dfrac 1 {\paren {2 k - 1}^2}$
It remains to be shown that:
:$\ds \lim_{n \mathop \to \infty} E_{2 n - 1} = 0$
which will establish:
:$\ds (5): \quad \dfrac {\pi^2} 8 = \sum_{k \mathop = 1}^n \dfrac 1 {\paren {2 k - 1}^2}$
Using $(2)$, let $\map g x$ be the function defined as:
:$\map g x := \map {\dfrac \d {\d x} } {\dfrac {x / 2} {\map \sin {x /2} } }$
Using Integration by Parts, we obtain:
:$\ds (6): \quad E_{2 n - 1} = \dfrac 1 {4 n - 1} \paren {2 + 2 \int_0^\pi \map g x \cos \dfrac {\paren {4 n - 1} x} 2 \rd x}$
during which we use {{Corollary|Limit of Sinc Function at Zero}}:
:$\ds \lim_{x \mathop \to 0} \dfrac {x / 2} {\map \sin {x / 2} } = 1$
We have that $\map g x$ is increasing on the interval of integration.
Therefore $\map g x$ is bounded on the interval $\closedint 0 \pi$ by $\map g \pi = \dfrac \pi 2$.
Hence $(5)$ has been established as being true.
Now we divide the (strictly) positive integers into even and odd, and use $(5)$ to obtain:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 1}^\infty \frac 1 {k^2}
      | r = \sum_{k \mathop = 1}^\infty \frac 1 {\paren {2 k}^2} + \sum_{k \mathop = 1}^\infty \frac 1 {\paren {2 k - 1}^2}
      | c = 
}}
{{eqn | r = \frac 1 4 \sum_{k \mathop = 1}^\infty \frac 1 {k^2} + \frac {\pi^2} 8
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac 3 4 \sum_{k \mathop = 1}^\infty \frac 1 {k^2}
      | r = \frac {\pi^2} 8
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sum_{k \mathop = 1}^\infty \frac 1 {k^2}
      | r = \frac 4 3 \frac {\pi^2} 8
      | c = 
}}
{{eqn | r = \frac {\pi^2} 6
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Basel Problem

:$\ds \map \zeta 2 = \sum_{n \mathop = 1}^\infty {\frac 1 {n^2} } = \frac {\pi^2} 6$
where $\zeta$ denotes the Riemann zeta function.

Proof:
{{begin-eqn}}
{{eqn | l = \map \zeta 2
      | r = \paren {-1}^2 \frac {B_2 2^1 \pi^2} {2!}
      | c = Riemann Zeta Function at Even Integers
}}
{{eqn | r = \paren {-1}^2 \paren {\frac 1 6} \frac {2^1 \pi^2} {2!}
      | c = {{Defof|Sequence of Bernoulli Numbers}}
}}
{{eqn | r = \paren {\frac 1 6} \paren {\frac 2 2} \pi^2
      | c = {{Defof|Factorial}}
}}
{{eqn | r = \frac {\pi^2} 6
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Basel Problem

:$\ds \map \zeta 2 = \sum_{n \mathop = 1}^\infty {\frac 1 {n^2} } = \frac {\pi^2} 6$
where $\zeta$ denotes the Riemann zeta function.

Proof:
By Fourier Series of $x^2$, for $x \in \openint {-\pi} \pi$:
:$\ds x^2 = \frac {\pi^2} 3 + \sum_{n \mathop = 1}^\infty \paren {\paren {-1}^n \frac 4 {n^2} \cos n x}$
Letting $x \to \pi$ from the left:
{{begin-eqn}}
{{eqn | l = \pi^2
      | r = \frac {\pi^2} 3 + \sum_{n \mathop = 1}^\infty \paren {\paren {-1}^n \frac 4 {n^2} \cos \pi x}
}}
{{eqn | l = \pi^2
      | r = \frac {\pi^2} 3 + \sum_{n \mathop = 1}^\infty \paren {\paren {-1}^n \paren {-1}^n \frac 4 {n^2} }
      | c = Cosine of Multiple of $\pi$
}}
{{eqn | l = \pi^2
      | r = \frac {\pi^2} 3 + 4 \sum_{n \mathop = 1}^\infty \frac 1 {n^2}
}}
{{eqn | ll= \leadsto
      | l = \frac {2 \pi^2} 3 
      | r = 4 \sum_{n \mathop = 1}^\infty \frac 1 {n^2}
}}
{{eqn | ll= \leadsto
      | l = \sum_{n \mathop = 1}^\infty \frac 1 {n^2}
      | r = \frac {\pi^2} 6
}}
{{end-eqn}}
{{qed}}
Theorem: Basel Problem

:$\ds \map \zeta 2 = \sum_{n \mathop = 1}^\infty {\frac 1 {n^2} } = \frac {\pi^2} 6$
where $\zeta$ denotes the Riemann zeta function.

Proof:
By Fourier Series of Identity Function over $-\pi$ to $\pi$, for $x \in \openint {-\pi} \pi$:
:$\ds x \sim 2 \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n + 1} } n \map \sin {n x}$
Hence:
{{begin-eqn}}
{{eqn | l = \frac 1 \pi \int_{-\pi}^\pi x^2 \rd x 
      | r = \sum_{n \mathop = 1}^\infty \paren {\frac{2 \paren {-1}^{n + 1} } n}^2
      | c = Parseval's Theorem
}}
{{eqn | ll= \leadsto
      | l = \frac 2 \pi \int_0^\pi x^2 \rd x 
      | r = \sum_{n \mathop = 1}^\infty \frac 4 {n^2}
      | c = Definite Integral of Even Function
}}
{{eqn | ll=\leadsto
      | l = \frac {2 \pi^2} 3 
      | r = \sum_{n \mathop = 1}^\infty \frac 4 {n^2} 
}}
{{eqn | ll=\leadsto
      | l = \sum_{n \mathop = 1}^\infty \frac 1 {n^2} 
      | r = \frac {\pi^2} 6 
}} 
{{end-eqn}}
{{qed}}
Theorem: Basel Problem

:$\ds \map \zeta 2 = \sum_{n \mathop = 1}^\infty {\frac 1 {n^2} } = \frac {\pi^2} 6$
where $\zeta$ denotes the Riemann zeta function.

Proof:
Let $\map f x$ be the real function defined on $\openint 0 {2 \pi}$ as:
:$\map f x = \begin {cases} \paren {x - \pi}^2 & : 0 < x \le \pi \\ \pi^2 & : \pi < x < 2 \pi \end {cases}$
From Fourier Series: Square of x minus pi, Square of pi, its Fourier series can be expressed as:
:$\map f x \sim \ds \dfrac {2 \pi^2} 3 + \sum_{n \mathop = 1}^\infty \paren {\frac {2 \cos n x} {n^2} + \paren {\frac {\paren {-1}^n \pi} n + \frac {2 \paren {\paren {-1}^n - 1} } {\pi n^3} } \sin n x}$
Setting $x = 0$:
{{begin-eqn}}
{{eqn | l = \map f 0
      | r = \frac {2 \pi^2} 3 + \sum_{n \mathop = 1}^\infty \paren {\frac {2 \cos 0} {n^2} + \paren {\frac {\paren {-1}^n \pi} n + \frac {2 \paren {\paren {-1}^n - 1} } {\pi n^3} } \sin 0}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {0 - \pi}^2
      | r = \frac {2 \pi^2} 3 + \sum_{n \mathop = 1}^\infty \paren {\frac {2 \cos 0} {n^2} }
      | c = Sine of Zero is Zero
}}
{{eqn | ll= \leadsto
      | l = \pi^2
      | r = \frac {2 \pi^2} 3 + 2 \sum_{n \mathop = 1}^\infty \frac 1 {n^2}
      | c = Cosine of Zero is One
}}
{{eqn | ll= \leadsto
      | l = \frac {\pi^2} 2 - \frac {\pi^2} 3
      | r = \sum_{n \mathop = 1}^\infty \frac 1 {n^2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\pi^2} 6
      | r = \sum_{n \mathop = 1}^\infty \frac 1 {n^2}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: 1+2+...+n+(n-1)+...+1 = n^2

:$\forall n \in \N: 1 + 2 + \cdots + n + \paren {n - 1} + \cdots + 1 = n^2$

Proof:
{{begin-eqn}}
{{eqn | o =
      | r = 1 + 2 + \cdots + \paren {n - 1} + n + \paren {n - 1} + \cdots + 1
      | c = 
}}
{{eqn | r = 1 + 2 + \cdots + \paren {n - 1} + \paren {n - 1} + \cdots + 1 + n
      | c = 
}}
{{eqn | r = 2 \paren {1 + 2 + \cdots + \paren {n - 1} } + n
      | c = 
}}
{{eqn | r = 2 \paren {\frac {\paren {n - 1} n} 2} + n
      | c = Closed Form for Triangular Numbers
}}
{{eqn | r = \paren {n - 1} n + n
      | c = 
}}
{{eqn | r = n^2 - n + n
      | c = 
}}
{{eqn | r = n^2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: 1+2+...+n+(n-1)+...+1 = n^2

:$\forall n \in \N: 1 + 2 + \cdots + n + \paren {n - 1} + \cdots + 1 = n^2$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = 1 + 2 + \cdots + \paren {n - 1} + n + \paren {n - 1} + \cdots + 1
      | c = 
}}
{{eqn | r = \paren {1 + 2 + \cdots + \paren {n - 1} } + \paren {1 + 2 + \cdots + \paren {n - 1} + n}
      | c = 
}}
{{eqn | r = \frac {\paren {n - 1} n} 2 + \frac {n \paren {n + 1} } 2
      | c = Closed Form for Triangular Numbers
}}
{{eqn | r = \frac {n^2 - n + n^2 + n} 2
      | c = 
}}
{{eqn | r = n^2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: 1+2+...+n+(n-1)+...+1 = n^2

:$\forall n \in \N: 1 + 2 + \cdots + n + \paren {n - 1} + \cdots + 1 = n^2$

Proof:
Proof by induction:
=== Basis for the Induction ===
$n = 1$ holds trivially.
Just to make sure, we try $n = 2$:
:$1 + 2 + 1 = 4$
Likewise $n^2 = 2^2 = 4$.
So shown for basis for the induction.
=== Induction Hypothesis ===
This is the induction hypothesis:
:$1 + 2 + \cdots + k + \paren {k - 1} + \cdots + 1 = k^2$
Now we need to show true for $n = k + 1$:
:$1 + 2 + \cdots + \paren {k + 1} + k + \paren {k - 1} + \cdots + 1 = \paren {k + 1}^2$
=== Induction Step ===
This is the induction step:
{{begin-eqn}}
{{eqn | o = 
      | r = 1 + 2 + \cdots + \paren {k + 1} + k + \paren {k - 1} + \cdots + 1
      | c = 
}}
{{eqn | r = \paren {1 + 2 + \cdots + k + \paren {k - 1} + \cdots + 1} + k + \paren {k + 1}
      | c = 
}}
{{eqn | r = k^2 + k + \paren {k + 1}
      | c = from induction hypothesis
}}
{{eqn | r = k^2 + 2k + 1
      | c = 
}}
{{eqn | r = \paren {k + 1}^2
      | c = 
}}
{{end-eqn}}
The result follows by induction.
{{qed}}
Theorem: 1+2+...+n+(n-1)+...+1 = n^2

:$\forall n \in \N: 1 + 2 + \cdots + n + \paren {n - 1} + \cdots + 1 = n^2$

Proof:
Let $T_n = 1 + 2 + \cdots + n + \paren {n - 1} + \cdots + 1$.
We have $T_1 = 1$
and
{{begin-eqn}}
{{eqn | l = T_n - T_{n - 1}
      | r = \paren {1 + 2 + \cdots + n + \paren {n - 1} + \cdots + 1 }
      | c = Definition of $T_n$
}}
{{eqn | o = 
      | ro= - 
      | r = \paren {1 + 2 + \cdots + \paren {n - 1} + \paren {n - 2} + \cdots + 1}
      | c = 
}}
{{eqn | r = \paren {\paren {1 + 2 + \cdots + n} - \paren {1 + 2 + \cdots + \paren {n - 1} } }
      | c = Integer Addition is Associative
}}
{{eqn | o = 
      | ro= + 
      | r = \paren {\paren {\paren {n - 1} + \paren {n - 2} + \cdots + 1} - \paren {\paren {n - 2} + \paren {n - 3} + \cdots + 1} }
      | c = Integer Addition is Commutative
}}
{{eqn | r = n + \paren {n - 1}
      | c = simplifying
}}
{{eqn | r = 2 n - 1
      | c = 
}}
{{end-eqn}}
Thus we have:
{{begin-eqn}}
{{eqn | l = T_n
      | r = \paren {T_n - T_{n - 1} } + \paren {T_{n - 1} - T_{n - 2} } + \cdots + \paren {T_2 - T_1} + T_1
}}
{{eqn | r = \paren {2 n - 1} + \paren {2 \paren {n - 1} - 1} + \cdots + \paren {2 \times 2 - 1} + 1
}}
{{eqn | r = \sum_{k \mathop = 1}^n 2 k - 1
}}
{{eqn | r = n^2 
      | c = Odd Number Theorem
}}
{{end-eqn}}
{{qed}}
Theorem: Necessary Conditions for Existence of Skolem Sequence

A Skolem sequence of order $n$ can only exist if $n \equiv 0, 1 \pmod 4$.

Proof:
Let $S$ be a Skolem sequence of order $n$.
Let $a_i$ and $b_i$ be the positions of the first and second occurrences respectively of the integer $i$ in $S$, where $1 \le i \le n$.
We can thus conclude that:
:$b_i - a_i = i$
for each $i$ from 1 to $n$.
Summing both sides of this equation we obtain:
:$\ds \sum_i^n b_i - \sum_i^n a_i = \sum_i^n i = \frac {n \paren {n + 1} } 2$
Now the $a_i$ and the $b_i$ represent the positions in the sequence from $1$ to $2 n$.
Hence:
:$\ds \sum_i^n b_i + \sum_i^n a_i = \frac {2 n \paren {2 n + 1} } 2 = n \paren {2 n + 1}$
Summing the previous two equations we obtain the identity:
:$\ds \sum_i^n b_i = \frac {n \paren {5 n + 3} } 4$
The {{LHS}} of this last equality is a sum of positions and thus must be an integer.
We conclude that the {{RHS}} must also be an integer.
This occurs exactly when:
$n \equiv 0, 1 \pmod 4$
{{qed}}
Theorem: Divisibility by 9

A number expressed in decimal notation is divisible by $9$ {{iff}} the sum of its digits is divisible by $9$.
That is:
:$N = \sqbrk {a_0 a_1 a_2 \ldots a_n}_{10} = a_0 + a_1 10 + a_2 10^2 + \cdots + a_n 10^n$ is divisible by $9$ 
{{iff}}:
:$a_0 + a_1 + \cdots + a_n$ is divisible by $9$.

Proof:
Let $N$ be divisible by $9$.
Then:
{{begin-eqn}}
{{eqn | l = N
      | o = \equiv
      | r = 0 \pmod 9
}}
{{eqn | ll= \leadstoandfrom
      | l = a_0 + a_1 10 + a_2 10^2 + \cdots + a_n 10^n
      | o = \equiv
      | r = 0 \pmod 9
}}
{{eqn | ll= \leadstoandfrom
      | l = a_0 + a_1 1 + a_2 1^2 + \cdots + a_n 1^n
      | o = \equiv
      | r = 0 \pmod 9
      | c = as $10 \equiv 1 \pmod 9$
}}
{{eqn | ll= \leadstoandfrom
      | l = a_0 + a_1 + \cdots + a_n
      | o = \equiv
      | r = 0 \pmod 9
}}
{{end-eqn}}
{{qed}}
Theorem: Divisibility by 9

A number expressed in decimal notation is divisible by $9$ {{iff}} the sum of its digits is divisible by $9$.
That is:
:$N = \sqbrk {a_0 a_1 a_2 \ldots a_n}_{10} = a_0 + a_1 10 + a_2 10^2 + \cdots + a_n 10^n$ is divisible by $9$ 
{{iff}}:
:$a_0 + a_1 + \cdots + a_n$ is divisible by $9$.

Proof:
This is a special case of Congruence of Sum of Digits to Base Less 1.
{{qed}}
Theorem: Existence of Rational Powers of Irrational Numbers

There exist irrational numbers $a$ and $b$ such that $a^b$ is rational.

Proof:
We have that:
: $\sqrt 2$ is irrational.
: $2$ is trivially rational, as $2 = \dfrac 2 1$.
Consider the number $q = \sqrt 2^{\sqrt 2}$, which is irrational by the Gelfond-Schneider Theorem.
Thus:
: $q^{\sqrt 2} = \left({\sqrt 2^{\sqrt 2}}\right)^{\sqrt 2} = \sqrt 2 ^{\left({\sqrt 2}\right) \left({\sqrt 2}\right)} = \sqrt 2^2 = 2$
is rational.
So $a = q = \sqrt 2^{\sqrt 2}$ and $b = \sqrt 2$ are the desired irrationals.
{{qed}}