階乗 \(n!\) は \(+\)・\(\cdot\)・\(\uparrow\) と同じく漸化式を満たす演算として仮定します（!𝕄）。列は写像 \(\mathbb{M} \to \mathbb{M}\) で、1点の値だけを変えた列が在ること（UPD）は word_basis の補題です。

1 逆元

自然数には引き算が無いので、\(xy \equiv 1 \pmod p\) を \(xy = pt + 1\) と書きます。

1.1 余りの一意性

1.2 逆元の一意性

1.3 逆元の存在

2 列の積

列の積（80 の \(f \prod k\)）について、値が全部1なら積は1、値が変わらなければ積も変わらない、1点の値を1に替えると積はその値で割ったものになる、を示します。

3 逆元の組

列 \(g\) の最初の \(n\) 項が「値は \(p\) 未満・1でない値には別の位置に逆元があり・1でない値は重ならない」ことを \(g \rightleftharpoons \langle p,n\rangle\) と書きます。
word(ss,s)F … \(\mathsf{pr}\)
abbr … \(\langle X , Y \rangle\) ≈ \(\mathsf{pr} ( X , Y )\)
word(ss,p) … \(\rightleftharpoons\)
⇌. … \(g \rightleftharpoons \langle p , n \rangle \Longleftrightarrow \forall i \in \mathbb{M} . ( i < n \Longrightarrow g ( i ) \in \mathbb{M} , g ( i ) < p ) , \forall i \in \mathbb{M} . ( i < n , g ( i ) \neq 1 \Longrightarrow \exists j \in \mathbb{M} . j < n , j \neq i , g ( j ) \neq 1 , \exists t \in \mathbb{M} . g ( i ) \cdot g ( j ) = p \cdot t + 1 ) , \forall i \in \mathbb{M} . \forall j \in \mathbb{M} . ( i < n , j < n , g ( i ) \neq 1 , g ( i ) = g ( j ) \Longrightarrow i = j )\)
\(g \rightleftharpoons \langle p,n\rangle\) なら積は \(p\) で割って1余ります。1でない値の位置のうち一番後ろの \(k\) と、その逆元の位置 \(j\) の値を1に替えても \(\rightleftharpoons\) のままなので、\(k\) についての帰納法で示します。
CLM … \(p \in \mathbb{P} , n \in \mathbb{M} , g \rightleftharpoons \langle p , n \rangle \Longrightarrow \exists t \in \mathbb{M} . g \prod n = p \cdot t + 1\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，Ldiv ，LG ，Euclid ，prod𝕄 ，UPD ，ONE ，STEP

4 主定理

\(p = n + 1\) を素数とします。列 \(f(i) = i + 1\)（\(i < n\)）の積は \(n!\) です。\(f\) の最後の値 \(n\) だけを1に替えた列 \(g\) は \(g \rightleftharpoons \langle p,n\rangle\) です（\(2 \le x < n\) の逆元 \(y\) は \(0\)・\(1\)・\(n\)・\(x\) のどれでもない）。よって \(n! = (pt + 1) \cdot n\) で、\(n! + 1 = p(tn + 1)\)。
Wilson の定理（Freek #51）：\(p = n + 1\) が素数なら \(p \mid n! + 1\)。
Wilson … \(p \in \mathbb{P} , n \in \mathbb{M} , p = ( n + 1 ) \Longrightarrow p \mid n ! + 1\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，Ldiv ，LG ，Euclid ，prod𝕄 ，UPD ，!𝕄 ，gcd𝕄 ，FAC ，EXG ，UPDp ，CLM ，START