1 主定理

word(ss,s)F … \(\)
自然数の公理と加法・乗法は 0.book のもの。そのうち suc𝕄（後続の単射性・\(0\) は後続でない）は使わない（主定理の前提の列に suc𝕄 が無い）。
\(s(n)\) を初項 \(a\)、公差 \(d\) の等差数列の最初の \(n\) 項の和とします。
ここでは \(s\) を \(s(0) = 0\) と漸化式を満たす関数として仮定します（\(a\)・\(d\) は自然数）。そのような \(s\) が存在することは示しません。したがって主定理は「そのような \(s\) があれば」という条件付きの形です（\(s\) が無ければ何も言っていません）。
形式的には \(s(i)\) の値がこの2式を満たすことだけを仮定し、\(s\) が写像であること（ap の定義）は使いません。
\(s(1) = a\)、\(s(2) = a + (a + d)\) です。主定理は最初の \(n+1\) 項の和 \(s(n+1)\)（最後の項は \(a + nd\)）について、割り算を使わず \(2s(n+1) = (n+1)(2a + nd)\) の形で述べます。
証明は \(n\) についての帰納法（IND𝕄）です。\(n = 0\) では両辺とも \(2a\)。\(n\) から \(n+1\) へは、漸化式と帰納法の仮定から
\(2s(n+2) = 2s(n+1) + 2(a + (n+1)d) = (n+1)(2a + nd) + 2(a + (n+1)d)\) で、分配・結合・交換法則により \(= (n+2)(2a + (n+1)d)\) です。
\(\begin{cases} a , d \in \mathbb{M} \\ s ( 0 ) = 0 \\ \forall i \in \mathbb{M} . s ( i \textit{+1} ) = s ( i ) + ( a + i \cdot d ) \end{cases} , n \in \mathbb{M} \Longrightarrow 2 \cdot s ( n \textit{+1} ) = ( n \textit{+1} ) \cdot ( 2 \cdot a + n \cdot d )\) \(\blacktriangleleft\) 𝕄0s ，IND𝕄 ，+𝕄 ，*𝕄 ，1. ，2.