剰余定理：多項式 \(P(x)\) について \(P(x) - P(a)\) は \(x - a\) で割り切れる。ここでは係数が自然数の多項式 \(P(x) = \sum_{i和は \(f\ \mathrm{sum}\ n\)（第 0 項から第 \(n-1\) 項まで）。

1 準備

歩みの等式：\((a + d)^{k+1} = a^{k+1} + d \left(a^k + r (a + d)\right)\)。
Lpc … \(a , d , k , r \in \mathbb{M} , ( a + d ) ^ k = a ^ k + d \cdot r \Longrightarrow ( a + d ) ^ ( k + 1 ) = a ^ ( k + 1 ) + d \cdot ( a ^ k + r \cdot ( a + d ) )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax+𝕄 ，⋅𝕄 ，↑𝕄
歩み。
Lps … \(a , d , k \in \mathbb{M} , \exists r \in \mathbb{M} . ( a + d ) ^ k = a ^ k + d \cdot r \Longrightarrow \exists r \in \mathbb{M} . ( a + d ) ^ ( k + 1 ) = a ^ ( k + 1 ) + d \cdot r\) \(\blacktriangleleft\) Lpc ，\(\mathbb{W}.\) ，Ax+𝕄 ，⋅𝕄 ，↑𝕄
\((a + d)^k = a^k + d r\)（\(k\) についての帰納法）。
Lpw … \(a , d \in \mathbb{M} \Longrightarrow \forall k \in \mathbb{M} . \exists r \in \mathbb{M} . ( a + d ) ^ k = a ^ k + d \cdot r\) \(\blacktriangleleft\) Lps ，\(\mathbb{W}.\) ，Ax+𝕄 ，⋅𝕄 ，↑𝕄

2 和

係数を掛けた和：\((V + dq) + c(A + dr) = (V + cA) + d(q + cr)\)。
Lrg … \(V , q , c , A , r , d \in \mathbb{M} \Longrightarrow ( V + d \cdot q ) + c \cdot ( A + d \cdot r ) = ( V + c \cdot A ) + d \cdot ( q + c \cdot r )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，INDC ，+𝕄 ，⋅𝕄 ，\(0 \in \mathbb{M}\)

3 剰余定理

底（\(n = 0\)）と歩み。
LB … \(a , d \in \mathbb{M} , \forall i \in \mathbb{M} . c ( i ) \in \mathbb{M} , u ( i ) = c ( i ) \cdot ( ( a + d ) ^ i ) , v ( i ) = c ( i ) \cdot ( a ^ i ) \Longrightarrow \exists q \in \mathbb{M} . ( u \sum 0 ) = ( v \sum 0 ) + d \cdot q\) \(\blacktriangleleft\) Lrg ，Lpw ，sum𝕄 ，\(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Ax+𝕄 ，⋅𝕄 ，ℙ.'
歩みの等式（\(q, r\) を取った形）。
LSc … \(a , d \in \mathbb{M} , \forall i \in \mathbb{M} . c ( i ) \in \mathbb{M} , u ( i ) = c ( i ) \cdot ( ( a + d ) ^ i ) , v ( i ) = c ( i ) \cdot ( a ^ i ) , n , q , r \in \mathbb{M} , ( u \sum n ) = ( v \sum n ) + d \cdot q , ( a + d ) ^ n = a ^ n + d \cdot r \Longrightarrow ( u \sum ( n + 1 ) ) = ( v \sum ( n + 1 ) ) + d \cdot ( q + c ( n ) \cdot r )\) \(\blacktriangleleft\) Lrg ，Lpw ，sum𝕄 ，\(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Ax+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.'
LS … \(a , d \in \mathbb{M} , \forall i \in \mathbb{M} . c ( i ) \in \mathbb{M} , u ( i ) = c ( i ) \cdot ( ( a + d ) ^ i ) , v ( i ) = c ( i ) \cdot ( a ^ i ) , n \in \mathbb{M} , \exists q \in \mathbb{M} . ( u \sum n ) = ( v \sum n ) + d \cdot q \Longrightarrow \exists q \in \mathbb{M} . ( u \sum ( n + 1 ) ) = ( v \sum ( n + 1 ) ) + d \cdot q\) \(\blacktriangleleft\) LSc ，Lrg ，Lpw ，sum𝕄 ，\(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Ax+𝕄 ，⋅𝕄 ，ℙ.'
すべての \(n\) について（帰納法）。
Lind … \(a , d \in \mathbb{M} , \forall i \in \mathbb{M} . c ( i ) \in \mathbb{M} , u ( i ) = c ( i ) \cdot ( ( a + d ) ^ i ) , v ( i ) = c ( i ) \cdot ( a ^ i ) \Longrightarrow \forall n \in \mathbb{M} . \exists q \in \mathbb{M} . ( u \sum n ) = ( v \sum n ) + d \cdot q\) \(\blacktriangleleft\) LB ，LS ，sum𝕄 ，\(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Ax+𝕄 ，⋅𝕄 ，ℙ.'

4 剰余定理

係数 \(c_i\) が自然数のとき、\(P(x) = \sum_{i \(a , d \in \mathbb{M} , \forall i \in \mathbb{M} . c ( i ) \in \mathbb{M} , u ( i ) = c ( i ) \cdot ( ( a + d ) ^ i ) , v ( i ) = c ( i ) \cdot ( a ^ i ) \Longrightarrow \forall n \in \mathbb{M} . \exists q \in \mathbb{M} . ( u \sum n ) = ( v \sum n ) + d \cdot q\) \(\blacktriangleleft\) Lind ，sum𝕄 ，\(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Ax+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.'