1 素数は二項係数を割る

\((k+1)\binom{n+1}{k+1} = (n+1)\binom{n}{k}\)（\(n\) についての帰納法）から、素数 \(p\) は \(0 \lt k \lt p\) のとき \(\binom{p}{k}\) を割ります（ユークリッドの補題）。
Labs … \(n , k \in \mathbb{M} \Longrightarrow ( k \textit{+1} ) \cdot ( ( n \textit{+1} ) \mathrm{C} ( k \textit{+1} ) ) = ( n \textit{+1} ) \cdot ( n \mathrm{C} k )\) \(\blacktriangleleft\) 𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄 ，*𝕄 ，choose𝕄 ，1.
∣choose … \(p \in \mathbb{P} , k , j \in \mathbb{M} , p = ( k \textit{+1} ) + ( j \textit{+1} ) \Longrightarrow p \mid p \mathrm{C} ( k \textit{+1} )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄 ，*𝕄 ，choose𝕄 ，1.

2 (a+1)^p と a^p+1

和 \(s(n)(m) = \sum_{k\lt m} \binom{n}{k} a^k\) を、44 と同じく漸化式を満たす関数として仮定します（存在は示しません）。二項定理（44）で \((a+1)^p = s(p)(p+1)\)。\(0\lt k\lt p\) の項は \(p\) で割り切れるので、\((a+1)^p\) は \(a^p+1\) と \(p\) の倍数だけ違います。したがって Fermat の小定理（主定理）は、前件「どの \(x\) にも和の関数 \(s\) がある」の下での条件付きの形です。
LF … \(\begin{cases} p \in \mathbb{P} \\ a \in \mathbb{M} \\ \forall n \in \mathbb{M} . s ( n ) ( 0 ) = 0 \\ \forall k \in \mathbb{M} . \forall j \in \mathbb{M} . s ( k + j ) ( k \textit{+1} ) = s ( k + j ) ( k ) + ( ( k + j ) \mathrm{C} k ) \cdot a ^ k \end{cases} \Longrightarrow \exists t \in \mathbb{M} . ( a + 1 ) ^ p = ( a ^ p + 1 ) + p \cdot t\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄 ，*𝕄 ，↑𝕄 ，choose𝕄 ，1.

3 Fermat の小定理

\(p\) が素数なら \(a^p\) は \(a\) と \(p\) の倍数だけ違う（\(a^p \equiv a \pmod p\)）。自然数には引き算が無いので \(a^p = a + pq\) と書きます。\(a\) についての帰納法で、\((a+1)^p = (a^p + 1) + pt = (a+1) + p(q+t)\)。
\(p \in \mathbb{P} , a \in \mathbb{M} , \forall x \in \mathbb{M} . \exists s ( \forall n \in \mathbb{M} . s ( n ) ( 0 ) = 0 , \forall k \in \mathbb{M} . \forall j \in \mathbb{M} . s ( k + j ) ( k \textit{+1} ) = s ( k + j ) ( k ) + ( ( k + j ) \mathrm{C} k ) \cdot x ^ k ) \Longrightarrow \exists q \in \mathbb{M} . a ^ p = a + p \cdot q\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄 ，*𝕄 ，↑𝕄 ，choose𝕄 ，1.