偶数の完全数は \(2^k q\)（\(q = 2^{k+1}-1\) は素数）の形：偶数 \(n = 2^a m\)（\(m\) は奇数）が完全数なら、\(\sigma(2^a m) = (2^{a+1}-1)\sigma(m) = 2^{a+1} m\) から \(m = (2^{a+1}-1)t\)、さらに \(\sigma(m) = 2^{a+1}t = m + t\) より \(t = 1\) で \(m\) は素数。
有限集合の補題：個数 0 の集合は空・個数 \(k+1\) の集合は空でなく、1点 \(x\) を除くと個数 \(k\)・\(A \setminus \{b\}\) の元は \(A\) の元で \(b\) でないもの。
Lb0 … \(X \stackrel{\#}= 0 \Longrightarrow X = \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s
Lne … \(k \in \mathbb{M} , X \stackrel{\#}= k + 1 \Longrightarrow \exists x \, x \in X\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s
Lrm … \(k \in \mathbb{M} , X \stackrel{\#}= k + 1 , x \in X \Longrightarrow X \mathop\setminus \{ x \} \stackrel{\#}= k , X \mathop\setminus \{ x \} \subset X , x \notin X \mathop\setminus \{ x \} , X = ( X \mathop\setminus \{ x \} ) \cup \{ x \}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s

1 有限集合の和

自然数の有限集合は上に有界。
Lbd … \(X \stackrel{\#}= k \in \mathbb{M} , X \subset \mathbb{M} \Longrightarrow \exists b \in \mathbb{M} . \forall y \in X . y \le b\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，Lb0 ，Lne ，Lrm
有界な2つの集合の和集合も有界。
Lub … \(X \subset \mathbb{M} , Y \subset \mathbb{M} , \exists b \in \mathbb{M} . \forall y \in X . y \le b , \exists c \in \mathbb{M} . \forall y \in Y . y \le c \Longrightarrow \exists d \in \mathbb{M} . \forall y \in X \cup Y . y \le d\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄
有限な自然数の集合の和は自然数（個数 \(k\) についての帰納法）。
Lsn … \(X \stackrel{\#}= k \in \mathbb{M} , X \subset \mathbb{M} \Longrightarrow \sum' X \in \mathbb{M}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，AxΣ ，Lb0 ，Lne ，Lrm ，Lbd
共通部分のない有限な \(X\)（\(a\) 個）と \(Y\)（\(k\) 個）について \(\sum (X \cup Y) = \sum X + \sum Y\)（\(k\) についての帰納法）。
Ladd … \(X \stackrel{\#}= a \in \mathbb{M} , X \subset \mathbb{M} , Y \stackrel{\#}= k \in \mathbb{M} , Y \subset \mathbb{M} , X \cap Y = \emptyset \Longrightarrow \sum' ( X \cup Y ) = \sum' X + \sum' Y\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，AxΣ ，Lb0 ，Lne ，Lrm ，Lbd ，Lub ，Lsn

2 倍

掛け算は順序を保つ。
Lmono … \(x , y , c \in \mathbb{M} , x \le y \Longrightarrow c \cdot x \le c \cdot y\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，AxΣ
個数 \(k\) の \(D \subset \mathbb{M}\) の各元を \(c\) 倍した集合 \(E\) の和は \(c\) 倍（\(k\) についての帰納法・\(c \neq 0\)）。
Lsc … \(D \stackrel{\#}= k \in \mathbb{M} , D \subset \mathbb{M} , c \in \mathbb{N} , \forall z \, ( z \in E \Longleftrightarrow \exists u \in D . z = c \cdot u ) \Longrightarrow \sum' E = c \cdot \sum' D\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，AxΣ ，Lb0 ，Lne ，∈∖1 ，Lrm ，Lbd ，Lsn ，Lmono

3 約数の集合

上に有界な自然数の集合は有限（0 から \(b\) までの区間の部分集合）。
Lfin … \(X \subset \mathbb{M} , b \in \mathbb{M} , \forall y \in X . y \le b \Longrightarrow \exists k \in \mathbb{M} . X \stackrel{\#}= k\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄
奇数 \(m\) について、\(2^j m\) の約数は \(2^i d\)（\(i \le j\)・\(d \mid m\)）の形（\(j\) についての帰納法・Lsplit）。
Lchar … \(m \in \mathbb{M} , j \in \mathbb{M} \Longrightarrow \forall e \in \mathbb{M} . ( e \mid 2 ^ j \cdot m \Longrightarrow \exists i \in \mathbb{M} . \exists d \in \mathbb{M} . i \le j , d \mid m , e = 2 ^ i \cdot d )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，↑𝕄 ，Lsplit ，L2↑
2 の冪：\(2^{i+t} = 2^i \cdot 2^t\)。\(i \le j\) なら \(2^i \mid 2^j\)。
Lpow2 … \(i , t \in \mathbb{M} \Longrightarrow 2 ^ ( i + t ) = 2 ^ i \cdot 2 ^ t\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，↑𝕄 ，Lsplit ，L2↑
Lpd … \(i , j \in \mathbb{M} , i \le j \Longrightarrow 2 ^ i \mid 2 ^ j\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，↑𝕄 ，Lsplit ，L2↑ ，Lpow2
\(2^i d \mid 2^j m\)（\(i \le j\)・\(d \mid m\)）。奇数 \(m\) では \(2^{j+1} u\) は \(2^j m\) を割らない。
L1d … \(i , j , d , m \in \mathbb{M} , i \le j , d \mid m \Longrightarrow 2 ^ i \cdot d \mid 2 ^ j \cdot m\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，↑𝕄 ，Lsplit ，L2↑ ，Lpow2 ，Lpd
L3d … \(j , u , m \in \mathbb{M} , \neg 2 \mid m , u \mid m \Longrightarrow \neg 2 ^ { ( j + 1 ) } \cdot u \mid 2 ^ j \cdot m\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，↑𝕄 ，Lsplit ，L2↑
奇数 \(m\) について \(\mathrm{Div}(2^{j+1} m) = \mathrm{Div}(2^j m) \sqcup 2^{j+1}\cdot\mathrm{Div}(m)\)。
LD1 … \(m , j \in \mathbb{M} , \forall z \, ( z \in T \Longleftrightarrow \exists u \in \mathrm{Div} m . z = 2 ^ { ( j + 1 ) } \cdot u ) \Longrightarrow \mathrm{Div} ( 2 ^ { ( j + 1 ) } \cdot m ) = \mathrm{Div} ( 2 ^ j \cdot m ) \cup T\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，↑𝕄 ，Lsplit ，L2↑ ，Lchar ，Lpow2 ，Lpd ，L1d
LD2 … \(m , j \in \mathbb{M} , \neg 2 \mid m , \forall z \, ( z \in T \Longleftrightarrow \exists u \in \mathrm{Div} m . z = 2 ^ { ( j + 1 ) } \cdot u ) \Longrightarrow \mathrm{Div} ( 2 ^ j \cdot m ) \cap T = \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，↑𝕄 ，Lsplit ，L2↑ ，L3d

4 約数の和の漸化式

\(n \neq 0\) の約数は \(n\) 以下で有限。
LDb … \(n \in \mathbb{N} \Longrightarrow \mathrm{Div} n \subset \mathbb{M} , \forall y \in \mathrm{Div} n . y \le n\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，↑𝕄 ，AxΣ ，Lsplit ，L2↑
LDfin … \(n \in \mathbb{N} \Longrightarrow \exists k \in \mathbb{M} . \mathrm{Div} n \stackrel{\#}= k\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，↑𝕄 ，AxΣ ，Lsplit ，L2↑ ，Lfin ，LDb
\(2^{j+1}\cdot\mathrm{Div}(m)\) も \(2^{j+1} m\) 以下で有限。
LTb … \(m , j \in \mathbb{M} , m \in \mathbb{N} , \forall z \, ( z \in T \Longleftrightarrow \exists u \in \mathrm{Div} m . z = 2 ^ { ( j + 1 ) } \cdot u ) \Longrightarrow T \subset \mathbb{M} , \forall z \in T . z \le 2 ^ { ( j + 1 ) } \cdot m , \exists k \in \mathbb{M} . T \stackrel{\#}= k\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，↑𝕄 ，AxΣ ，Lsplit ，L2↑ ，Lmono ，Lfin ，LDb
\(\sigma(2^{j+1} m) = \sigma(2^j m) + 2^{j+1}\sigma(m)\)（\(m\) は奇数）。
LSig … \(m , j \in \mathbb{M} , m \in \mathbb{N} , \neg 2 \mid m \Longrightarrow \sum' ( \mathrm{Div} ( 2 ^ { ( j + 1 ) } \cdot m ) ) = \sum' ( \mathrm{Div} ( 2 ^ j \cdot m ) ) + 2 ^ { ( j + 1 ) } \cdot \sum' ( \mathrm{Div} m )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，↑𝕄 ，AxΣ ，Lsplit ，L2↑ ，Lb0 ，Lne ，∈∖1 ，Lrm ，Lbd ，Lub ，Lsn ，Ladd ，Lmono ，Lsc ，Lfin ，Lchar ，Lpow2 ，Lpd ，L1d ，L3d ，LD1 ，LD2 ，LDb ，LDfin ，LTb

5 約数の和の等式

約数の和は自然数。
LSn … \(n \in \mathbb{N} \Longrightarrow \sum' ( \mathrm{Div} n ) \in \mathbb{M}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，↑𝕄 ，AxΣ ，Lsplit ，L2↑ ，Lb0 ，Lne ，Lrm ，Lbd ，Lsn ，Lfin ，LDb ，LDfin
\(\sigma(2^j m) + \sigma(m) = 2^{j+1}\sigma(m)\)（\(m\) は奇数・引き算なし。\(j\) についての帰納法）。
LSig2 … \(m , j \in \mathbb{M} , m \in \mathbb{N} , \neg 2 \mid m \Longrightarrow \sum' ( \mathrm{Div} ( 2 ^ j \cdot m ) ) + \sum' ( \mathrm{Div} m ) = 2 ^ { ( j + 1 ) } \cdot \sum' ( \mathrm{Div} m )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，↑𝕄 ，AxΣ ，Lsplit ，L2↑ ，Lb0 ，Lne ，∈∖1 ，Lrm ，Lbd ，Lub ，Lsn ，Ladd ，Lmono ，Lsc ，Lfin ，Lchar ，Lpow2 ，Lpd ，L1d ，L3d ，LD1 ，LD2 ，LDb ，LDfin ，LTb ，LSig ，LSn

6 分解

0 でない自然数は \(2^a m\)（\(m\) は奇数）の形（強い帰納法）。
Ldec … \(n \in \mathbb{N} \Longrightarrow \exists a \in \mathbb{M} . \exists m \in \mathbb{N} . n = 2 ^ a \cdot m , \neg 2 \mid m\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，↑𝕄 ，L2↑

7 本体

\(m \in \mathbb{N}\) の約数の和は、真の約数の和 \(t\) と \(m\) 自身の和。
LG1 … \(m \in \mathbb{N} \Longrightarrow \exists t \in \mathbb{M} . \sum' ( \mathrm{Div} m ) = t + m , \sum' ( \mathrm{Div} m \mathop\setminus \{ m \} ) = t\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，↑𝕄 ，AxΣ ，Lsplit ，L2↑ ，Lb0 ，Lne ，∈∖1 ，Lrm ，Lbd ，Lsn ，Lfin ，LDb
\(\sigma(2^a m) = 2 \cdot 2^a m\) と \(\sigma(m) = t + m\) から \(m + t = 2^{a+1} t\)。
LG2 … \(m , a , t \in \mathbb{M} , m \in \mathbb{N} , \neg 2 \mid m , \sum' ( \mathrm{Div} ( 2 ^ a \cdot m ) ) = 2 \cdot ( 2 ^ a \cdot m ) , \sum' ( \mathrm{Div} m ) = t + m \Longrightarrow m + t = 2 ^ { ( a + 1 ) } \cdot t\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，↑𝕄 ，AxΣ ，Lsplit ，L2↑ ，Lb0 ，Lne ，∈∖1 ，Lrm ，Lbd ，Lub ，Lsn ，Ladd ，Lmono ，Lsc ，Lfin ，Lchar ，Lpow2 ，Lpd ，L1d ，L3d ，LD1 ，LD2 ，LDb ，LDfin ，LTb ，LSig ，LSn ，LSig2
\(a \ge 1\) なら \(2^{a+1} \ge 4\)。\(q + 1 = 2^{a+1}\) とおくと \(m + t = (q+1)t\) から \(m = q t\)（\(q \ge 3\)）。
LG3 … \(m , a , t \in \mathbb{M} , \neg a = 0 , m + t = 2 ^ { ( a + 1 ) } \cdot t \Longrightarrow \exists q \in \mathbb{M} . q + 1 = 2 ^ { ( a + 1 ) } , m = q \cdot t , \neg q = 0 , \neg q = 1\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，↑𝕄 ，AxΣ ，Lsplit ，L2↑
要素がすべて 0 でない有限集合 \(X\) の和が \(t \in X\) に等しければ、\(X\) の元は \(t\) だけ。
Lone … \(k \in \mathbb{M} , X \stackrel{\#}= k + 1 , X \subset \mathbb{M} , \forall y \in X . \neg y = 0 , t \in X , \sum' X = t , e \in X \Longrightarrow e = t\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，↑𝕄 ，AxΣ ，Lsplit ，L2↑ ，Lb0 ，Lne ，∈∖1 ，Lrm ，Lbd ，Lsn
\(m = q t\)（\(q \neq 0, 1\)）なら \(t\) は \(m\) の真の約数。
LH1 … \(m , q , t \in \mathbb{M} , m \in \mathbb{N} , m = q \cdot t , \neg q = 0 , \neg q = 1 \Longrightarrow t \in \mathbb{N} , \neg t = m , \neg m = 1 , t \mid m\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，↑𝕄 ，AxΣ ，Lsplit ，L2↑
真の約数の和が \(t\)（\(t\) は \(m\) の真の約数）なら \(t = 1\)。真の約数は \(t\) だけで、\(1\) も真の約数だから。
LH2 … \(m \in \mathbb{N} , t \in \mathbb{N} , t \mid m , \neg t = m , \neg m = 1 , \sum' ( \mathrm{Div} m \mathop\setminus \{ m \} ) = t \Longrightarrow t = 1\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，↑𝕄 ，AxΣ ，Lsplit ，L2↑ ，Lb0 ，Lne ，∈∖1 ，Lrm ，Lbd ，Lsn ，Lfin ，LDb ，Lone
真の約数の和が \(1\) なら \(m\) は素数（真の約数は \(1\) だけ）。
LH3 … \(m \in \mathbb{N} , \neg m = 1 , \sum' ( \mathrm{Div} m \mathop\setminus \{ m \} ) = 1 \Longrightarrow m \in \mathbb{P}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，↑𝕄 ，AxΣ ，Lsplit ，L2↑ ，Lb0 ，Lne ，∈∖1 ，Lrm ，Lbd ，Lsn ，Lfin ，LDb ，Lone
偶数の完全数 \(n = 2^a m\)（\(m\) は奇数）は \(m + t = 2^{a+1} t\)・\(m = q t\)（\(q = 2^{a+1} - 1\)）。
LMb … \(m , a \in \mathbb{M} , m \in \mathbb{N} , \neg 2 \mid m , \neg a = 0 , \sum' ( \mathrm{Div} ( 2 ^ a \cdot m ) ) = 2 \cdot ( 2 ^ a \cdot m ) \Longrightarrow \exists t \in \mathbb{M} . \exists q \in \mathbb{M} . \sum' ( \mathrm{Div} m \mathop\setminus \{ m \} ) = t , ( q + 1 = 2 ^ { ( a + 1 ) } ) , m = q \cdot t , \neg q = 0 , \neg q = 1\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，↑𝕄 ，AxΣ ，Lsplit ，L2↑ ，Lb0 ，Lne ，∈∖1 ，Lrm ，Lbd ，Lub ，Lsn ，Ladd ，Lmono ，Lsc ，Lfin ，Lchar ，Lpow2 ，Lpd ，L1d ，L3d ，LD1 ，LD2 ，LDb ，LDfin ，LTb ，LSig ，LSn ，LSig2 ，LG1 ，LG2 ，LG3

8 主定理（オイラー）

偶数の完全数（約数の和が自身の2倍）は \(2^a q\)（\(q = 2^{a+1} - 1\) は素数）の形。
\(n \in \mathbb{N} , 2 \mid n , \sum' ( \mathrm{Div} n ) = 2 \cdot n \Longrightarrow \exists a \in \mathbb{M} . \exists q \in \mathbb{P} . ( q + 1 = 2 ^ { ( a + 1 ) } ) , n = 2 ^ a \cdot q\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，↑𝕄 ，AxΣ ，Lsplit ，L2↑ ，Lb0 ，Lne ，∈∖1 ，Lrm ，Lbd ，Lub ，Lsn ，Ladd ，Lmono ，Lsc ，Lfin ，Lchar ，Lpow2 ，Lpd ，L1d ，L3d ，LD1 ，LD2 ，LDb ，LDfin ，LTb ，LSig ，LSn ，LSig2 ，Ldec ，LG1 ，LG2 ，LG3 ，Lone ，LH1 ，LH2 ，LH3 ，LMb