調和級数 \(\displaystyle \sum_{k=1}^{n} \frac{1}{k}\) は \(n\) を大きくすればいくらでも大きくなる。部分和の列 \(h(n)\) を漸化式 \(h(0) = 0\)、\(h(n+1) = h(n) + \frac{1}{n+1}\) で与える。\(h(a + m) \ge h(a) + \frac{m}{a+m}\)（\(m\) についての帰納法）から \(h(2n) \ge h(n) + \frac12\)、よって \(h(2^k) \ge \frac{k}{2}\)。

1 1つ分の分数

\(\frac{m}{d} = \frac{m}{d+1} + \frac{m}{d(d+1)}\)。
Lc … \(m , d \in \mathbb{M} , d \in \mathbb{N} \Longrightarrow m / d = ( m / ( d + 1 ) ) + ( m / ( d \cdot ( d + 1 ) ) )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ ，≤ℚ

2 列の値は有理数

Lde … \(a \in \mathbb{Z} , b \in \mathbb{N} \Longrightarrow a / b \in \mathbb{Q}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ ，≤ℚ
LQb … \({h} ( 0 ) = 0 , \forall n \in \mathbb{M} . {h} ( n + 1 ) = {h} ( n ) + ( 1 / ( n + 1 ) ) \Longrightarrow {h} ( 0 ) \in \mathbb{Q}\) \(\blacktriangleleft\) Lde ，\(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ ，≤ℚ
LQs … \({h} ( 0 ) = 0 , \forall n \in \mathbb{M} . {h} ( n + 1 ) = {h} ( n ) + ( 1 / ( n + 1 ) ) , n \in \mathbb{M} , {h} ( n ) \in \mathbb{Q} \Longrightarrow {h} ( n + 1 ) \in \mathbb{Q}\) \(\blacktriangleleft\) Lde ，\(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ ，≤ℚ
LQ … \({h} ( 0 ) = 0 , \forall n \in \mathbb{M} . {h} ( n + 1 ) = {h} ( n ) + ( 1 / ( n + 1 ) ) \Longrightarrow \forall n \in \mathbb{M} . {h} ( n ) \in \mathbb{Q}\) \(\blacktriangleleft\) LQb ，LQs ，Lde ，\(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ ，≤ℚ

3 分数の計算

\(\frac{m+1}{e} = \frac{m}{e} + \frac{1}{e}\)。
Lsp … \(m \in \mathbb{M} , e \in \mathbb{N} \Longrightarrow ( m + 1 ) / e = ( m / e ) + ( 1 / e )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ ，≤ℚ
有理数の足し算の組み替え。
Lag … \(A , P , Q , U , W \in \mathbb{Q} \Longrightarrow ( ( A + ( P + Q ) ) + U ) + W = ( A + ( P + W ) ) + ( Q + U )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ ，≤ℚ

4 部分和の下からの評価

\(h(a + m) = h(a) + \frac{m}{a+m} + (\text{正の数})\)。
Lan … \(a \in \mathbb{N} , m \in \mathbb{M} \Longrightarrow a + m \in \mathbb{N}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ ，≤ℚ
2つの分数を1つにまとめる。
Lu … \(m , d , u , v \in \mathbb{M} , d \in \mathbb{N} , v \in \mathbb{N} \Longrightarrow ( m / ( d \cdot ( d + 1 ) ) ) + ( u / v ) = ( m \cdot v + u \cdot ( d \cdot ( d + 1 ) ) ) / ( ( d \cdot ( d + 1 ) ) \cdot v ) , m \cdot v + u \cdot ( d \cdot ( d + 1 ) ) \in \mathbb{M} , ( d \cdot ( d + 1 ) ) \cdot v \in \mathbb{N}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ ，≤ℚ
LTc … \({h} ( 0 ) = 0 , \forall n \in \mathbb{M} . {h} ( n + 1 ) = {h} ( n ) + ( 1 / ( n + 1 ) ) , a \in \mathbb{N} , m \in \mathbb{M} , u \in \mathbb{M} , v \in \mathbb{N} , {h} ( a + m ) = ( {h} ( a ) + ( m / ( a + m ) ) ) + ( u / v ) \Longrightarrow {h} ( a + ( m + 1 ) ) = ( {h} ( a ) + ( ( m + 1 ) / ( a + ( m + 1 ) ) ) ) + ( ( m \cdot v + u \cdot ( ( a + m ) \cdot ( ( a + m ) + 1 ) ) ) / ( ( ( a + m ) \cdot ( ( a + m ) + 1 ) ) \cdot v ) )\) \(\blacktriangleleft\) Lc ，Lu ，LQ ，Lsp ，Lag ，Lan ，Lde ，\(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ ，≤ℚ
LTs … \({h} ( 0 ) = 0 , \forall n \in \mathbb{M} . {h} ( n + 1 ) = {h} ( n ) + ( 1 / ( n + 1 ) ) , a \in \mathbb{N} , m \in \mathbb{M} , \exists u \in \mathbb{M} . \exists v \in \mathbb{N} . {h} ( a + m ) = ( {h} ( a ) + ( m / ( a + m ) ) ) + ( u / v ) \Longrightarrow \exists u \in \mathbb{M} . \exists v \in \mathbb{N} . {h} ( a + ( m + 1 ) ) = ( {h} ( a ) + ( ( m + 1 ) / ( a + ( m + 1 ) ) ) ) + ( u / v )\) \(\blacktriangleleft\) LTc ，Lu ，Lan ，\(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ ，≤ℚ
底（\(m = 0\)）：\(h(a) = h(a) + 0 + 0\)。
LTb … \({h} ( 0 ) = 0 , \forall n \in \mathbb{M} . {h} ( n + 1 ) = {h} ( n ) + ( 1 / ( n + 1 ) ) , a \in \mathbb{N} \Longrightarrow \exists u \in \mathbb{M} . \exists v \in \mathbb{N} . {h} ( a + 0 ) = ( {h} ( a ) + ( 0 / ( a + 0 ) ) ) + ( u / v )\) \(\blacktriangleleft\) LQ ，Lan ，\(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ ，≤ℚ
\(m\) についての帰納法：\(h(a + m) = h(a) + \frac{m}{a+m} + \frac{u}{v}\)（\(u \in \mathbb{M}\)、\(v \in \mathbb{N}\)）。
LT … \({h} ( 0 ) = 0 , \forall n \in \mathbb{M} . {h} ( n + 1 ) = {h} ( n ) + ( 1 / ( n + 1 ) ) , a \in \mathbb{N} \Longrightarrow \forall m \in \mathbb{M} . \exists u \in \mathbb{M} . \exists v \in \mathbb{N} . {h} ( a + m ) = ( {h} ( a ) + ( m / ( a + m ) ) ) + ( u / v )\) \(\blacktriangleleft\) LTb ，LTs ，\(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ ，≤ℚ
倍にすると \(\frac12\) 以上増える：\(h(n + n) = h(n) + \frac12 + (\text{正の数})\)。
L2 … \({h} ( 0 ) = 0 , \forall n \in \mathbb{M} . {h} ( n + 1 ) = {h} ( n ) + ( 1 / ( n + 1 ) ) , n \in \mathbb{N} \Longrightarrow \exists u \in \mathbb{M} . \exists v \in \mathbb{N} . {h} ( n + n ) = ( {h} ( n ) + ( 1 / 2 ) ) + ( u / v )\) \(\blacktriangleleft\) LT ，Lan ，\(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ ，≤ℚ

5 2 のべき乗

組み替え：\(((P + U) + H) + V = (P + H) + (U + V)\)。
Lrg … \(P , U , H , V \in \mathbb{Q} \Longrightarrow ( ( P + U ) + H ) + V = ( P + H ) + ( U + V )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ ，≤ℚ
2 のべき乗は正の整数。
Lp2n … \(k \in \mathbb{M} \Longrightarrow 2 ^ k \in \mathbb{N}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ ，≤ℚ ，↑𝕄
\(2^{k+1} = 2^k + 2^k\)。
Lp2 … \(k \in \mathbb{M} \Longrightarrow 2 ^ ( k + 1 ) = ( 2 ^ k ) + ( 2 ^ k )\) \(\blacktriangleleft\) Lp2n ，\(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ ，≤ℚ ，↑𝕄

6 調和数の下からの評価

\(h(2^{k}) = \frac{k}{2} + (\text{正の数})\) が成り立てば \(h(2^{k+1}) = \frac{k+1}{2} + (\text{正の数})\)。
LDc … \(k , u , v , u_{1} , v_{1} \in \mathbb{M} , v \in \mathbb{N} , v_{1} \in \mathbb{N} , {h} ( 2 ^ k ) = ( k / 2 ) + ( u / v ) , {h} ( ( 2 ^ k ) + ( 2 ^ k ) ) = ( {h} ( 2 ^ k ) + ( 1 / 2 ) ) + ( u_{1} / v_{1} ) , {h} ( 2 ^ k ) \in \mathbb{Q} \Longrightarrow \exists w \in \mathbb{M} . \exists z \in \mathbb{N} . {h} ( 2 ^ ( k + 1 ) ) = ( ( k + 1 ) / 2 ) + ( w / z )\) \(\blacktriangleleft\) Lp2 ，Lsp ，Lrg ，Lde ，\(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ ，≤ℚ
底（\(k = 0\)）：\(h(1) = 1\)。
LDb … \({h} ( 0 ) = 0 , \forall n \in \mathbb{M} . {h} ( n + 1 ) = {h} ( n ) + ( 1 / ( n + 1 ) ) \Longrightarrow \exists u \in \mathbb{M} . \exists v \in \mathbb{N} . {h} ( 2 ^ 0 ) = ( 0 / 2 ) + ( u / v )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ ，≤ℚ ，↑𝕄
歩み。
LDs … \({h} ( 0 ) = 0 , \forall n \in \mathbb{M} . {h} ( n + 1 ) = {h} ( n ) + ( 1 / ( n + 1 ) ) , k \in \mathbb{M} , \exists u \in \mathbb{M} . \exists v \in \mathbb{N} . {h} ( 2 ^ k ) = ( k / 2 ) + ( u / v ) \Longrightarrow \exists u \in \mathbb{M} . \exists v \in \mathbb{N} . {h} ( 2 ^ ( k + 1 ) ) = ( ( k + 1 ) / 2 ) + ( u / v )\) \(\blacktriangleleft\) LDc ，L2 ，Lp2n ，LQ ，Lan ，\(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ ，≤ℚ ，↑𝕄
LD … \({h} ( 0 ) = 0 , \forall n \in \mathbb{M} . {h} ( n + 1 ) = {h} ( n ) + ( 1 / ( n + 1 ) ) \Longrightarrow \forall k \in \mathbb{M} . \exists u \in \mathbb{M} . \exists v \in \mathbb{N} . {h} ( 2 ^ k ) = ( k / 2 ) + ( u / v )\) \(\blacktriangleleft\) LDb ，LDs ，\(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ ，≤ℚ ，↑𝕄

7 仕上げ

\(y = x + \frac{a}{b}\)（\(a \in \mathbb{M}\)、\(b \in \mathbb{N}\)）なら \(x \le y\)。
Le … \(x \in \mathbb{Q} , a \in \mathbb{M} , b \in \mathbb{N} , y = x + ( a / b ) \Longrightarrow x \le y\) \(\blacktriangleleft\) Lde ，\(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ ，≤ℚ ，↑𝕄
\(\frac{2N}{2} = N\)。
L2N … \(N \in \mathbb{M} \Longrightarrow ( 2 \cdot N ) / 2 = N\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ ，≤ℚ ，↑𝕄

8 調和級数の発散

部分和 \(h(n)\) は、どんな自然数 \(N\) も超える：\(N \le h(2^{2N})\)（\(h(2^k) \ge k/2\)）。
\({h} ( 0 ) = 0 , \forall n \in \mathbb{M} . {h} ( n + 1 ) = {h} ( n ) + ( 1 / ( n + 1 ) ) \Longrightarrow \forall N \in \mathbb{M} . \exists n \in \mathbb{M} . N \le {h} ( n )\) \(\blacktriangleleft\) LD ，Le ，L2N ，Lp2n ，\(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，÷ℚ ，+ℚ ，⋅ℚ ，≤ℚ ，↑𝕄