avewright/proofwiki-math huggingface dataset:
Theorem: Sequence of General Harmonic Numbers Converges for Index Greater than 1

Let $\map {H^{\paren r} } n$ denote the general harmonic number:
:$\ds \map {H^{\paren r} } n = \sum_{k \mathop = 1}^n \frac 1 {k^r}$
for $r \in \R_{>0}$.
Let $r > 1$.
Then as $n \to \infty$, $\map {H^{\paren r} } n$ is convergent with an upper bound of $\dfrac {2^{r - 1} } {2^{r - 1} - 1}$.

Proof:
Let $m \in \N$ be arbitrary.
Then:
{{begin-eqn}}
{{eqn | l = \harm r {2^{m - 1} }
      | r = \harm r {2^{m - 1} - 1} + \dfrac 1 {\paren {2^{m - 1} }^r} + \dfrac 1 {\paren {2^{m - 1} + 1}^r} + \cdots + \dfrac 1 {\paren {2^{m - 1} + \paren {2^{m - 1} - 1} }^r}
      | c = 
}}
{{eqn | o = <
      | r = \harm r {2^{m - 1} - 1} + \dfrac 1 {\paren {2^{m - 1} }^r} + \dfrac 1 {\paren {2^{m - 1} }^r} + \cdots + \dfrac 1 {\paren {2^{m - 1} }^r}
      | c = Ordering of Reciprocals
}}
{{eqn | r = \harm r {2^{m - 1} - 1} + \dfrac {2^{m - 1} } {2^{\paren {m - 1} r} }
      | c = 
}}
{{eqn | r = \harm r {2^{m - 1} - 1} + \paren {2^{1 - r} }^{m - 1}
      | c = 
}}
{{eqn | o = <
      | r = \harm r {2^{m - 2} - 1} + \paren {2^{1 - r} }^{m - 2} + \paren {2^{1 - r} }^{m - 1}
      | c = 
}}
{{eqn | o = <
      | r = \dots
      | c = 
}}
{{eqn | o = <
      | r = \harm r {2^0 - 1} + \paren {2^{1 - r} }^0 + \paren {2^{1 - r} }^1 + \dots + \paren {2^{1 - r} }^{m - 1}
      | c = 
}}
{{eqn | r = 0 + \sum_{k \mathop = 0}^{m - 1} \paren {2^{1 - r} }^k
}}
{{eqn | r = \dfrac {1 - \paren {2^{1 - r} }^m} {1 - 2^{1 - r} }
      | c = Sum of Geometric Sequence
}}
{{eqn | o = <
      | r = \dfrac 1 {1 - 2^{1 - r} }
      | c = as $0 < 2^{1 - r} < 1$
}}
{{eqn | r = \dfrac {2^{r - 1} } {2^{r - 1} - 1}
      | c = 
}}
{{end-eqn}}
Since $m$ is arbitrary, every partial sum $\harm r n$ is bounded from above by $\dfrac {2^{r - 1} } {2^{r - 1} - 1}$.
By the Monotone Convergence Theorem, as $n \to \infty$, $\harm r n$ is convergent with an upper bound of $\dfrac {2^{r - 1} } {2^{r - 1} - 1}$.
{{qed}}
Theorem: Inductive Construction of Sigma-Algebra Generated by Collection of Subsets

Let $\EE$ be a set of sets which are subsets of some set $X$.
Let $\map \sigma \EE$ be the $\sigma$-algebra generated by $\EE$.
Then $\map \sigma \EE$  can be constructed inductively.
The construction is as follows:
Let $\Omega$ denote the minimal uncountable well-ordered set.
Let $\alpha$ be an arbitrary initial segment in $\Omega$.
Considering separately the cases whether or not $\alpha$ has an immediate predecessor $\beta$, we define:
:$\EE_1 = \EE$
:$<nowiki>\EE_\alpha = \begin{cases} \set {\SS \in \powerset {\EE_\beta}: \SS \text { is countable or } \SS^\complement \text{ is countable} } & \alpha \text{ has an immediate predecessor } \beta \\
\ds \bigcup_{\beta \mathop \prec \alpha} \EE_\beta & \text { otherwise} \end{cases}</nowiki>$
:$\EE_\Omega = \ds \bigcup_{\alpha \mathop \in \Omega} \EE_\alpha$
Then:
:$\map \sigma \EE = \EE_\Omega$

Proof:
=== Step 1 ===
We will show that:
:$\map \sigma \EE \subseteq \EE_\Omega$.
Define: 
:$\OO := \set {o \in \Omega: \EE_o \in \map \sigma \EE}$
By the definition of a $\sigma$-algebra:
:$\EE_1 \subseteq \map \sigma \EE$.
From $\sigma$-Algebra of Countable Sets, if $\beta$ immediately precedes $\alpha$, then $\EE_\alpha$ is a $\sigma$-algebra containing $\EE_\beta$.
If $\beta$ strictly precedes $\alpha$ but is not an immediate predecessor of $\alpha$, then $\EE_\alpha$ is a countable union of measurable sets.
By the definition of a $\sigma$-algebra and of union, $\EE_\alpha$ is a $\sigma$-algebra containing $\EE_\beta$.
Thus the hypotheses of well-ordered induction are satisfied, and:
:$\OO = \Omega$
Thus:
:$\EE_\alpha \subseteq \map \sigma \EE$ 
for all $\alpha \in \Omega$
By Set Union Preserves Subsets:General Result:
:$\ds \bigcup_{\alpha \mathop \in \Omega} \EE_\alpha \subseteq \map \sigma \EE$
Thus:
:$\EE_{\Omega} \subseteq \map \sigma \EE$
{{qed|lemma}}
Theorem: Generating Function for Bernoulli Polynomials

Let $\map {B_n} x$ denote the $n$th Bernoulli polynomial.
Then the generating function for $B_n$ is:
:$\ds \frac {t e^{t x} } {e^t - 1} = \sum_{k \mathop = 0}^\infty \frac {\map {B_k} x} {k!} t^k$

Proof:
By definition of the generating function for Bernoulli numbers:
:$\ds \frac t {e^t - 1} = \sum_{k \mathop = 0}^\infty \frac {B_k} {k!} t^k$
By Power Series Expansion for Exponential Function:
:$\ds e^{t x} = \sum_{k \mathop = 0}^\infty \frac {x^k} {k!} t^k$
Thus:
:$\ds \frac {t e^{t x} } {e^t - 1} = \paren {\sum_{k \mathop = 0}^\infty \frac {B_k} {k!} t^k} \paren {\sum_{k \mathop = 0}^\infty \frac {x^k} {k!} t^k}$
Combining like powers of $t$ we obtain: 
{{begin-eqn}}
{{eqn | l = \frac {t e^{t x} } {e^t - 1}
      | r = \sum_{k \mathop = 0}^\infty t^k \sum_{m \mathop = 0}^k \frac {B_{k - m} } {\paren {k - m}!} \frac {x^m} {m!}
}}
{{eqn | r = \sum_{k \mathop = 0}^\infty \frac {t^k} {k!} \sum_{m \mathop = 0}^k \frac {k!} {\paren {k - m}! m!} B_{k - m} x^m
}}
{{eqn | r = \sum_{k \mathop = 0}^\infty \frac {t^k} {k!} \sum_{m \mathop = 0}^k \binom k m B_{k - m} x^m 
      | c = {{Defof|Binomial Coefficient|subdef = Integers|index = 1}}
}}
{{eqn | r = \sum_{k \mathop = 0}^\infty \frac {\map {B_k} x} {k!} t^k
      | c = {{Defof|Bernoulli Polynomial}}
}}
{{end-eqn}}
{{qed}}
Category:Bernoulli Polynomials
Category:Examples of Generating Functions
tbclk9vtxo8ccygw5ugeb0xtovrpgij
Theorem: Symmetry of Bernoulli Polynomial

Let $\map {B_n} x$ denote the nth Bernoulli polynomial.
Then:
:$\map {B_n} {1 - x} = \paren {-1}^n \map {B_n} x$

Proof:
Let $\map G {t, x}$ denote the Generating Function for Bernoulli Polynomials:
:$\map G {t, x} = \dfrac {t e^{t x} } {e^t - 1}$
Then:
{{begin-eqn}}
{{eqn | l = \map G {t, 1 - x}
      | r = \frac {t e^{t \paren {1 - x} } } {e^t - 1}
}}
{{eqn | r = \frac {t e^{t - t x} } {e^t - 1}
}}
{{eqn | r = \frac {t e^{-t x} } {1 - e^{-t} }
}}
{{eqn | r = \frac {-t e^{-t x} } {e^{-t} - 1}
}}
{{eqn | r = \map G {-t, x}
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \map G {t, 1 - x}
      | r = \map G {-t, x}
}}
{{eqn | ll= \leadsto
      | l = \sum_{k \mathop = 0}^\infty \frac {\map {B_k} {1 - x} } {k!} t^k 
      | r = \sum_{k \mathop = 0}^\infty \frac {\paren {-1}^k \map {B_k} x} {k!} t^k 
}}
{{eqn | ll= \leadsto
      | l = \map {B_k} {1 - x}
      | r = \paren {-1}^k \map {B_k} x
}}
{{end-eqn}}
{{qed}}
Category:Bernoulli Polynomials
abllm91bcr3elf7zkdfpxunc10isi65
Theorem: Value of Odd Bernoulli Polynomial at One Half

Let $\map {B_n} x$ denote the $n$th Bernoulli polynomial.
Then:
:$\map {B_{2 n + 1} } {\dfrac 1 2} = 0$

Proof:
{{begin-eqn}}
{{eqn | l = \map {B_{2 n + 1} } {1 - x}
      | r = \paren {-1}^{2 n + 1} \map {B_{2 n + 1} } x
      | c = Symmetry of Bernoulli Polynomial
}}
{{eqn | r = \paren {-1} \map {B_{2 n + 1} } x
}}
{{eqn | ll= \leadsto
      | l = \map {B_{2 n + 1} } {\frac 1 2}
      | r = \paren {-1} \map {B_{2 n + 1} } {\frac 1 2}
}}
{{eqn | ll= \leadsto
      | l = 2 \map {B_{2 n + 1} } {\frac 1 2}
      | r = 0
}}
{{eqn | l = \map {B_{2 n + 1} } {\frac 1 2}
      | r = 0
}}
{{end-eqn}}
{{qed}}
Category:Bernoulli Polynomials
8ho7t94ptmhs1n0r1tmopzw2icqam3e
Theorem: Harmonic Number is Greater than Logarithm plus Gamma

:$H_n > \ln n + \gamma$
where:
:$H_n$ denotes the $n$th harmonic number
:$\gamma$ denotes the Euler-Mascheroni constant.

Proof:
From Approximate Size of Sum of Harmonic Series:
:$H_n \approx \ln n + \gamma + \dfrac 1 {2 n} - \dfrac 1 {12 n^2} + \dfrac 1 {120 n^4} - \epsilon$
where $0 < \epsilon < \dfrac 1 {252 n^6}$.
We have that:
:$\dfrac 1 {2 n} + \dfrac 1 {120 n^4} > \dfrac 1 {12 n^2} + \dfrac 1 {252 n^6}$
and the result follows.
{{qed}}
Theorem: Summation to n of Power of k over k

:$\ds \sum_{k \mathop = 1}^n \dfrac {x^k} k = H_n + \sum_{k \mathop = 1}^n \dbinom n k \dfrac {\paren {x - 1}^k} k$
where:
:$H_n$ denotes the $n$th harmonic number
:$\dbinom n k$ denotes a binomial coefficient.

Proof:
Differentiating {{WRT|Differentiation}} $x$:
{{begin-eqn}}
{{eqn | l = \dfrac \d {\d x} \paren {\sum_{k \mathop = 1}^n \dfrac {x^k} k}
      | r = \sum_{k \mathop = 1}^n\dfrac \d {\d x}\paren {\dfrac {x^k} k}
      | c = Applications of Linear Combination of Derivatives
}}
{{eqn | r = \sum_{k \mathop = 1}^n k \dfrac {x^{k - 1} } k
      | c = Power Rule for Derivatives
}}
{{eqn | r = \sum_{k \mathop = 1}^n x^{k - 1}
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 0}^{n - 1} x^k
      | c = Translation of Index Variable of Summation
}}
{{eqn | r = \dfrac {x^n - 1} {x - 1}
      | c = Sum of Geometric Sequence
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 1}^n \dfrac {x^k} k
      | r = \int \dfrac {x^n - 1} {x - 1} \rd x
      | c = 
}}
{{eqn | r = \int \dfrac {\paren {z + 1}^n - 1} z \rd z
      | c = Integration by Substitution: $z = x - 1$
}}
{{eqn | r = \int \paren {\dfrac {\paren {z + 1}^n} z - \dfrac 1 z} \rd z
      | c = 
}}
{{eqn | r = \int \paren {\dfrac 1 z \sum_{k \mathop = 0}^n \dbinom n k z^k - \dfrac 1 z} \rd z
      | c = Binomial Theorem
}}
{{eqn | r = \int \paren {\sum_{k \mathop = 1}^n \dbinom n k z^{k - 1} + \dfrac 1 z - \dfrac 1 z} \rd z
      | c = Binomial Coefficient with Zero
}}
{{eqn | r = \int \paren {\sum_{k \mathop = 1}^n \dbinom n k z^{k - 1} } \rd z
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 1}^n \dbinom n k \int z^{k - 1} \rd z
      | c = Linear Combination of Primitives
}}
{{eqn | r = \sum_{k \mathop = 1}^n \dbinom n k \dfrac {z^k} k + C
      | c = Primitive of Power
}}
{{eqn | r = \sum_{k \mathop = 1}^n \dbinom n k \dfrac {\paren {x - 1}^k} k + C
      | c = 
}}
{{end-eqn}}
When $x = 1$ we have:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 1}^n \dbinom n k \dfrac {\paren {1 - 1}^k} k + C
      | r = \sum_{k \mathop = 1}^n \dfrac {1^k} k
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 0 + C
      | r = \sum_{k \mathop = 1}^n \dfrac 1 k
      | c = 
}}
{{eqn | ll= \leadsto
      | l = C
      | r = H_n
      | c = {{Defof|Harmonic Number}}
}}
{{end-eqn}}
The result follows.
Theorem: Harmonic Number as Unsigned Stirling Number of First Kind over Factorial

:$H_n = \dfrac { {n + 1} \brack 2} {n!}$
where:
:$H_n$ denotes the $n$th harmonic number
:$n!$ denotes the $n$th factorial
:$\ds { {n + 1} \brack 2}$ denotes an unsigned Stirling number of the first kind.

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$H_n = \dfrac { {n + 1} \brack 2} {n!}$
$\map P 0$ is the case:
{{begin-eqn}}
{{eqn | l = H_0
      | r = 0
      | c = 
}}
{{eqn | r = \dfrac {1 \brack 2} {0!}
      | c = Unsigned Stirling Number of the First Kind of Number with Greater
}}
{{end-eqn}}
Thus $\map P 0$ is seen to hold.
Theorem: Sum of Harmonic Numbers approaches Harmonic Number of Product of Indices

Let $m, n \in \Z_{>0}$ be (strictly) positive integers.
Let:
:$\map T {m, n} := H_m + H_n - H_{m n}$
where $H_n$ denotes the $n$th harmonic number.
Then as $m$ or $n$ increases, $\map T {m, n}$ never increases, and reaches its minimum when $m$ and $n$ approach infinity.

Proof:
{{begin-eqn}}
{{eqn | l = \map T {m + 1, n} - \map T {m, n}
      | r = \left({H_{m + 1} + H_n - H_{\paren {m + 1} n} }\right) - \paren {H_m + H_n - H_{m n} }
      | c = 
}}
{{eqn | r = \dfrac 1 {m + 1} + \paren {H_{\paren {m + 1} n} - H_{m n} }
      | c = 
}}
{{eqn | r = \dfrac 1 {m + 1} - \paren {\frac 1 {m n + 1} + \frac 1 {m n + 2} + \cdots + \frac 1 {m n + n} }
      | c = 
}}
{{eqn | o = \le
      | r = \dfrac 1 {m + 1} - \paren {\frac 1 {m n + n} + \frac 1 {m n + n} + \cdots + \frac 1 {m n + n} }
      | c = 
}}
{{eqn | r = \dfrac 1 {m + 1} - \frac n {n \paren {m + 1} }
      | c = 
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
Similarly:
:$\map T {m, n + 1} - \map T {m, n} \le 0$
From Approximate Size of Sum of Harmonic Series, the limiting value of $\map T {m, n}$ is the Euler-Mascheroni constant:
:$\ds \lim_{m, n \mathop \to \infty} H_m + H_n - H_{m n} = \gamma$
{{qed}}
Theorem: Summation over k to n of Natural Logarithm of k

:$\ds \sum_{k \mathop = 1}^n \ln k = \map \ln {n!}$
where $n!$ denotes the $n$th factorial.

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 1}^n \ln k
      | r = \ln \prod_{k \mathop = 1}^n k
      | c = Summation of General Logarithms
}}
{{eqn | r = \map \ln {n!}
      | c = {{Defof|Factorial}}
}}
{{end-eqn}}
{{qed}}
Theorem: Difference between Summation of Natural Logarithms and Summation of Harmonic Numbers

:$\ds \sum_{k \mathop = 1}^n H_k - \sum_{k \mathop = 1}^n \map \ln {n!} \approx \gamma n + \dfrac {\ln n} 2 + 0 \cdotp 158$
where:
:$H_k$ denotes the $k$th harmonic number
:$n!$ denotes the $n$th factorial
:$\gamma$ denotes the Euler-Mascheroni constant.

Proof:
From Summation over k to n of Natural Logarithm of k:
:$\ds \sum_{k \mathop = 1}^n \ln k = \map \ln {n!}$
Then:
{{begin-eqn}}
{{eqn | l = \map \ln {n!}
      | o = \approx
      | r = \map \ln {\sqrt {2 \pi n} \paren {\dfrac n e}^n}
      | c = Stirling's Formula
}}
{{eqn | r = \frac 1 2 \map \ln {2 \pi} + \frac 1 2 \ln n + n \paren {\ln n - \ln e}
      | c = 
}}
{{eqn | r = \map \ln {\sqrt {2 \pi} } + \paren {n + \frac 1 2} \ln n - n
      | c = 
}}
{{end-eqn}}
Then we have that:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 1}^n H_k
      | r = \paren {n + 1} H_n - n
      | c = Sum of Sequence of Harmonic Numbers
}}
{{eqn | o = \approx
      | r = \paren {n + 1} \paren {\ln n + \gamma + \dfrac 1 {2 n} - \dfrac 1 {12 n^2} + \dfrac 1 {120 n^4} } - n
      | c = Approximate Size of Sum of Harmonic Series
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | o = 
      | r = \sum_{k \mathop = 1}^n H_k - \sum_{k \mathop = 1}^n \map \ln {n!}
      | c = 
}}
{{eqn | o = \approx
      | r = \paren {\paren {n + 1} \paren {\ln n + \gamma + \dfrac 1 {2 n} - \dfrac 1 {12 n^2} + \dfrac 1 {120 n^4} } - n} - \paren {\ln \paren {\sqrt {2 \pi} } + \paren {n + \frac 1 2} \ln n - n}
      | c = 
}}
{{eqn | r = n \ln n + n \gamma + \dfrac 1 2 - \dfrac 1 {12 n} + \dfrac 1 {120 n^3} + \ln n + \gamma + \dfrac 1 {2 n} - \dfrac 1 {12 n^2} + \dfrac 1 {120 n^4} - n - \map \ln {\sqrt {2 \pi} } - n \ln n - \frac 1 2 \ln n + n
      | c = 
}}
{{eqn | r = \gamma n + \frac 1 2 \ln n + \dfrac 1 2 + \gamma - \map \ln {\sqrt {2 \pi} } + \dfrac 5 {12 n} - \dfrac 1 {12 n^2}  + \dfrac 1 {120 n^3} + \dfrac 1 {120 n^4}
      | c = 
}}
{{end-eqn}}
The result follows by ignoring the lower order terms in $n$.
{{qed}}
Theorem: Sum over k of n Choose k by x to the k by kth Harmonic Number/x = -1

While for $x \in \R_{>0}$ be a real number:
:$\ds \sum_{k \mathop \in \Z} \binom n k x^k H_k = \paren {x + 1}^n \paren {H_n - \map \ln {1 + \frac 1 x} } + \epsilon$
when $x = -1$ we have:
:$\ds \sum_{k \mathop \in \Z} \binom n k x^k H_k = \dfrac {-1} n$
where:
:$\dbinom n k$ denotes a binomial coefficient
:$H_k$ denotes the $k$th harmonic number.

Proof:
When $x = -1$ we have that $1 + \dfrac 1 x = 0$, so $\map \ln {1 + \dfrac 1 x}$ is undefined.
Let $S_n = \ds \sum_{k \mathop \in \Z} \binom n k x^k H_k$
Then:
{{begin-eqn}}
{{eqn | l = S_{n + 1}
      | r = \sum_{k \mathop \in \Z} \binom {n + 1} k x^k H_k
      | c = 
}}
{{eqn | r = \sum_{k \mathop \in \Z} \paren {\binom n k + \binom n {k - 1} } x^k H_k
      | c = Pascal's Rule
}}
{{eqn | r = S_n + x \sum_{k \mathop \ge 1} \paren {\binom n {k - 1} } x^{k - 1} \paren {H_{k - 1} + \frac 1 k}
      | c = 
}}
{{eqn | r = S_n + x S_n + \sum_{k \mathop \ge 1} \binom n {k - 1} x^k \frac 1 k
      | c = 
}}
{{eqn | r = \paren {1 + x} S_n + \frac 1 {n + 1} \sum_{k \mathop \ge 1} \binom {n + 1} k x^k
      | c = (look up result for this)
}}
{{end-eqn}}
{{LinkWanted|for the above}}
Setting $x = -1$:
{{begin-eqn}}
{{eqn | l = S_{n + 1}
      | r = \paren {1 + -1} S_n + \frac 1 {n + 1} \sum_{k \mathop \ge 1} \binom {n + 1} k \paren {-1}^k
      | c = 
}}
{{eqn | r = \frac 1 {n + 1} \sum_{k \mathop \ge 1} \binom {n + 1} k \paren {-1}^k
      | c = 
}}
{{eqn | ll= \leadsto
      | l = S_n
      | r = \frac 1 n \sum_{k \mathop \ge 1} \binom n k \paren {-1}^k
      | c = 
}}
{{eqn | r = \frac 1 n \paren {\sum_{k \mathop \ge 0} \binom n k \paren {-1}^k - \binom n 0}
      | c = 
}}
{{eqn | r = \frac 1 n \paren {0 - \binom n 0}
      | c = Alternating Sum and Difference of Binomial Coefficients for Given n
}}
{{eqn | r = \frac {-1} n
      | c = Binomial Coefficient with Zero
}}
{{end-eqn}}
{{qed}}
Theorem: Summation to n of Reciprocal of k by k-1 of Harmonic Number

:$\ds \sum_{1 \mathop < k \mathop \le n} \dfrac 1 {k \paren {k - 1} } H_k = 2 - \dfrac {H_n} n - \dfrac 1 n$
where $H_n$ denotes the $n$th harmonic number.

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{1 \mathop < k \mathop \le n} \dfrac 1 {k \paren {k - 1} } H_k
      | r = \sum_{k \mathop = 1}^{n - 1} \dfrac 1 {\paren {k + 1} k} H_{k + 1}
      | c = Translation of Index Variable of Summation
}}
{{eqn | r = -\sum_{k \mathop = 1}^{n - 1} \paren {\dfrac 1 {k + 1} - \dfrac 1 k} H_{k + 1}
      | c = 
}}
{{eqn | r = -\paren {\dfrac {H_{n + 1} } n - \dfrac {H_2} 1 - \sum_{k \mathop = 1}^{n - 1} \dfrac 1 {k + 1} \paren {H_{k + 2} - H_{k + 1} } } 
      | c = Abel's Lemma: Formulation 1
}}
{{eqn | r = H_2 - \dfrac {H_{n + 1} } n + \sum_{k \mathop = 1}^{n - 1} \dfrac 1 {k + 1} \dfrac 1 {k + 2}
      | c = simplification
}}
{{eqn | r = \frac 3 2 - \dfrac {H_{n + 1} } n + \sum_{k \mathop = 1}^{n - 1} \paren {\dfrac 1 {k + 1} - \dfrac 1 {k + 2} }
      | c = separating the fractions, and Harmonic Number $H_2$
}}
{{eqn | r = \frac 3 2 - \dfrac {H_{n + 1} } n + \frac 1 2 - \dfrac 1 {n + 1}
      | c = Telescoping Series
}}
{{eqn | r = 2 - \frac 1 n \paren {H_n + \dfrac 1 {n + 1} } - \dfrac 1 {n + 1}
      | c = 
}}
{{eqn | r = 2 - \frac {H_n} n - \dfrac 1 {n \paren {n + 1} } - \dfrac 1 {n + 1}
      | c = 
}}
{{eqn | r = 2 - \frac {H_n} n - \paren {\dfrac 1 n - \dfrac 1 {n + 1} } - \dfrac 1 {n + 1}
      | c = 
}}
{{eqn | r = 2 - \frac {H_n} n - \dfrac 1 n
      | c = after simplification
}}
{{end-eqn}}
{{qed}}
Theorem: Riemann Zeta Function of 1000

To at least $100$ decimal places:
:$\map \zeta {1000} \approx 1$
where $\zeta$ denotes the Riemann zeta function.

Proof:
By definition of the general harmonic numbers:
:$\ds \map \zeta r = \lim_{n \mathop \to \infty} H_n^{\paren r} = \sum_{k \mathop \ge 1} \frac 1 {k^r}$
From Sequence of General Harmonic Numbers Converges for Index Greater than 1:
{{begin-eqn}}
{{eqn | l = \map \zeta {1000}
      | o = \le
      | r = \dfrac {2^{1000} } {2^{1000} - 1}
      | c = 
}}
{{eqn | r = \dfrac 1 {1 - 2^{-1000} }
      | c = 
}}
{{end-eqn}}
which is $1 \cdot 000 \ldots$ to a good few hundred decimal places.
{{qed}}
Theorem: Summation to n of kth Harmonic Number over k

:$\ds \sum_{k \mathop = 1}^n \dfrac {H_k} k = \dfrac { {H_n}^2 + \harm 2 n } 2$
where:
:$H_n$ denotes the $n$th harmonic number
:$\harm 2 n$ denotes the general harmonic number of order $2$ evaluated at $n$.

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 1}^n \dfrac {H_k} k
      | r = \sum_{k \mathop = 1}^n \dfrac 1 k \sum_{j \mathop = 1}^k \dfrac 1 j
      | c = {{Defof|Harmonic Number}}
}}
{{eqn | r = \sum_{k \mathop = 1}^n \sum_{j \mathop = 1}^k \dfrac 1 j \dfrac 1 k
      | c = 
}}
{{eqn | r = \dfrac 1 2 \paren {\paren {\sum_{k \mathop = 1}^n \dfrac 1 k}^2 + \paren {\sum_{k \mathop = 1}^n \dfrac 1 {k^2} } }
      | c = Summation of Products of $n$ Numbers taken $m$ at a time with Repetitions: Order $2$
}}
{{eqn | r = \dfrac { {H_n}^2 + \harm 2 n } 2
      | c = {{Defof|Harmonic Number}} and {{Defof|General Harmonic Numbers}}
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Summation to n of kth Harmonic Number over k+1

:$\ds \sum_{k \mathop = 1}^n \dfrac {H_k} {k + 1} = \dfrac { {H_{n + 1} }^2 - \harm 2 {n + 1} } 2$
where:
:$H_n$ denotes the $n$th harmonic number
:$\harm 2 n$ denotes the general harmonic number of order $2$ evaluated at $n$.

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 1}^n \dfrac {H_k} {k + 1}
      | r = \sum_{k \mathop = 1}^n \dfrac 1 {k + 1} \paren {H_{k + 1} - \dfrac 1 {\paren {k + 1} } }
      | c = {{Defof|Harmonic Number}}
}}
{{eqn | r = \sum_{k \mathop = 1}^n \paren {\dfrac {H_{k + 1} } {k + 1} - \dfrac 1 {\paren {k + 1} \paren {k + 1} } }
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 1}^n \dfrac {H_{k + 1} } {k + 1} - \sum_{k \mathop = 1}^n \dfrac 1 {\paren {k + 1}^2}
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 2}^{n + 1} \dfrac {H_k} k - \sum_{k \mathop = 2}^{n + 1} \dfrac 1 {k^2}
      | c = Translation of Index Variable of Summation
}}
{{eqn | r = \sum_{k \mathop = 1}^{n + 1} \dfrac {H_k} k - \dfrac {H_1} 1 - \paren{\sum_{k \mathop = 1}^{n + 1} \dfrac 1 {k^2} - \dfrac 1 {1^2} }
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 1}^{n + 1} \dfrac {H_k} k - 1 - \paren{\sum_{k \mathop = 1}^{n + 1} \dfrac 1 {k^2} - 1}
      | c = Harmonic Number $H_1$
}}
{{eqn | r = \sum_{k \mathop = 1}^{n + 1} \dfrac {H_k} k - \sum_{k \mathop = 1}^{n + 1} \dfrac 1 {k^2}
      | c = simplifying
}}
{{eqn | r = \sum_{k \mathop = 1}^{n + 1} \dfrac {H_k} k - \harm 2 {n + 1}
      | c = {{Defof|General Harmonic Numbers}}
}}
{{eqn | r = \dfrac { {H_{n + 1} }^2 + \harm 2 {n + 1} } 2 -  \harm 2 {n + 1}
      | c = Summation to n of kth Harmonic Number over k
}}
{{eqn | r = \dfrac { {H_{n + 1} }^2 + \harm 2 {n + 1} - 2 \harm 2 {n + 1} } 2
      | c = 
}}
{{eqn | r = \dfrac { {H_{n + 1} }^2 - \harm 2 {n + 1} } 2
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Sum of External Angles of Polygon equals Four Right Angles

Let the external angles of a polygon be generated in the same direction going around the polygon.
Then the sum of all these external angles equals $4$ right angles, that is, $360 \degrees$.

Proof:
Let $V$ be an arbitrary vertex of a polygon $P$.
Let $T$ be the sum of all the external angles of $P$
Let $A$ be the size of the internal angle of $V$.
Let $E$ be the size of the external angle of $V$.
By definition, $E = 180 \degrees - A$.
Let $S$ denote the sum of all internal angles of $P$.
Hence we have:
:$T = n \times 180 \degrees - S$
From Sum of Internal Angles of Polygon:
:$S = \paren {n - 2} 180 \degrees$
Hence we have:
{{begin-eqn}}
{{eqn | l = T
      | r = n \times 180 \degrees - \paren {n - 2} 180 \degrees
      | c = 
}}
{{eqn | r = n \times 180 \degrees - n \times 180 \degrees + 2 \times 180 \degrees
      | c = multiplying out
}}
{{eqn | r = 360 \degrees
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Bisector of Apex of Isosceles Triangle also Bisects Base

Let $\triangle ABC$ be an isosceles triangle whose apex is $A$.
Let $AD$ be the bisector of $\angle BAC$ such that $AD$ intersects $BC$ at $D$.
Then $AD$ bisects $BC$.

Proof:
By definition of isosceles triangle, $AB = AC$.
By definition of bisector, $\angle BAD = \angle CAD$.
By construction, $AD$ is common.
Thus by Triangle Side-Angle-Side Congruence, $\triangle ABD = \triangle ACD$.
Thus $AD = DC$.
The result follows by definition of bisection.
{{qed}}
Theorem: Bisector of Apex of Isosceles Triangle is Perpendicular to Base

Let $\triangle ABC$ be an isosceles triangle whose apex is $A$.
Let $AD$ be the bisector of $\angle BAC$ such that $AD$ intersects $BC$ at $D$.
Then $AD$ is perpendicular to $BC$.

Proof:
By definition of isosceles triangle, $AB = AC$.
By definition of bisector, $\angle BAD = \angle CAD$.
By construction, $AD$ is common.
Thus by Triangle Side-Angle-Side Congruence, $\triangle ABD = \triangle ACD$.
Thus $\angle ADB = \angle ADC$.
By Two Angles on Straight Line make Two Right Angles, $\angle ADB + \angle ADC$ equals $2$ right angles.
Thus each of $\angle ADB$ and $\angle ADC$ are right angles.
The result follows by definition of perpendicular.
{{qed}}
Theorem: Equilateral Triangle is Equiangular

Let $\triangle ABC$ be an equilateral triangle.
Then $\triangle ABC$ is also equiangular, with each internal angle equal to $60 \degrees$.

Proof:
Let $\triangle ABC$ be an equilateral triangle.
By definition of equilateral triangle, any two of the sides of $\triangle ABC$ are equal.
{{WLOG}}, let $AB = AC$.
Then by Isosceles Triangle has Two Equal Angles:
:$\angle ABC = \angle ACB$
As the choice of equal sides was arbitrary, it follows that every two of the internal angles of $\triangle ABC$ are equal.
Hence all $3$ internal angles of $\triangle ABC$ are equal.
{{qed|lemma}}
From Sum of Angles of Triangle equals Two Right Angles, the internal angles of $\triangle ABC$ all add up to $180 \degrees$.
Hence it follows that one such internal angle is $\dfrac {180 \degrees} 3$, or $60 \degrees$.
{{qed}}