1 準備

階乗 \(n!\) は \(+\)・\(\cdot\)・\(\uparrow\) と同じく漸化式を満たす演算として仮定します（!𝕄）。列の1点の値だけを変えた列があること（upd𝕄・73・31 と同じ）も仮定します。
word(s,s) … \(!\)
!𝕄 … \(\begin{cases} 0 ! = 1 \\ n \in \mathbb{M} \Longrightarrow ( n \textit{+1} ) ! = n ! \cdot n \textit{+1} \end{cases}\)
upd𝕄 … \(\exists g \, ( g ( k ) = p , \forall i \in \mathbb{M} . ( i \neq k \Longrightarrow g ( i ) = f ( i ) ) )\)

2 逆元

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

2.1 余りの一意性

2.2 逆元の一意性

2.3 逆元の存在

3 列の積

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

4 逆元の組

列 \(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}.\) ，𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄 ，*𝕄 ，1. ，prod𝕄 ，upd𝕄

5 主定理

\(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 \textit{+1} \Longrightarrow p \mid n ! + 1\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄 ，*𝕄 ，1. ，prod𝕄 ，!𝕄 ，upd𝕄 ，gcd𝕄