---

Step * 1 1 2 1 1 1 1 of Lemma wilson-theorem


1. n : {i:ℤ| 1 < i} 
2. prime(n)
3. ∀b:ℕn. ((rotate-by(n;1) (rotate-by(n;n - 1) b)) = b ∈ ℕn)
4. ∀b:ℕn. ((rotate-by(n;n - 1) (rotate-by(n;1) b)) = b ∈ ℕn)
5. cyclic-map(ℕn) ~ ℕ(n - 1)!
6. a1 : ℕn ⟶ ℕn
7. Inj(ℕn;ℕn;a1)
8. ∀x,y:ℕn.  ∃n@0:ℕ. ((a1^n@0 x) = y ∈ ℕn)
9. a2 : ℕn →⟶ ℕn
10. ∀x,y:ℕn.  ∃n@0:ℕ. ((a2^n@0 x) = y ∈ ℕn)
11. (rotate-by(n;n - 1) o (a1 o rotate-by(n;1))) = (rotate-by(n;n - 1) o (a2 o rotate-by(n;1))) ∈ cyclic-map(ℕn)
12. (rotate-by(n;1) o ((rotate-by(n;n - 1) o (a1 o rotate-by(n;1))) o rotate-by(n;n - 1)))
= (rotate-by(n;1) o ((rotate-by(n;n - 1) o (a2 o rotate-by(n;1))) o rotate-by(n;n - 1)))
∈ cyclic-map(ℕn)
⊢ a1 = a2 ∈ (ℕn ⟶ ℕn)
BY
{ ((Ext THEN Auto) THEN ApFunToHypEquands `Z' ⌜Z x⌝ ⌜ℕn⌝ (-2)⋅ THEN Reduce (-1) THEN Auto) }

1
1. n : {i:ℤ| 1 < i} 
2. prime(n)
3. ∀b:ℕn. ((rotate-by(n;1) (rotate-by(n;n - 1) b)) = b ∈ ℕn)
4. ∀b:ℕn. ((rotate-by(n;n - 1) (rotate-by(n;1) b)) = b ∈ ℕn)
5. cyclic-map(ℕn) ~ ℕ(n - 1)!
6. a1 : ℕn ⟶ ℕn
7. Inj(ℕn;ℕn;a1)
8. ∀x,y:ℕn.  ∃n@0:ℕ. ((a1^n@0 x) = y ∈ ℕn)
9. a2 : ℕn →⟶ ℕn
10. ∀x,y:ℕn.  ∃n@0:ℕ. ((a2^n@0 x) = y ∈ ℕn)
11. (rotate-by(n;n - 1) o (a1 o rotate-by(n;1))) = (rotate-by(n;n - 1) o (a2 o rotate-by(n;1))) ∈ cyclic-map(ℕn)
12. (rotate-by(n;1) o ((rotate-by(n;n - 1) o (a1 o rotate-by(n;1))) o rotate-by(n;n - 1)))
= (rotate-by(n;1) o ((rotate-by(n;n - 1) o (a2 o rotate-by(n;1))) o rotate-by(n;n - 1)))
∈ cyclic-map(ℕn)
13. x : ℕn
14. (rotate-by(n;1) (rotate-by(n;n - 1) (a1 (rotate-by(n;1) (rotate-by(n;n - 1) x)))))
= (rotate-by(n;1) (rotate-by(n;n - 1) (a2 (rotate-by(n;1) (rotate-by(n;n - 1) x)))))
∈ ℕn
⊢ (a1 x) = (a2 x) ∈ ℕn

---

Latex:

---

Latex:

1.  n  :  \{i:\mBbbZ{}|  1  <  i\} 
2.  prime(n)
3.  \mforall{}b:\mBbbN{}n.  ((rotate-by(n;1)  (rotate-by(n;n  -  1)  b))  =  b)
4.  \mforall{}b:\mBbbN{}n.  ((rotate-by(n;n  -  1)  (rotate-by(n;1)  b))  =  b)
5.  cyclic-map(\mBbbN{}n)  \msim{}  \mBbbN{}(n  -  1)!
6.  a1  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n
7.  Inj(\mBbbN{}n;\mBbbN{}n;a1)
8.  \mforall{}x,y:\mBbbN{}n.    \mexists{}n@0:\mBbbN{}.  ((a1\^{}n@0  x)  =  y)
9.  a2  :  \mBbbN{}n  \mrightarrow{}{}\mrightarrow{}  \mBbbN{}n
10.  \mforall{}x,y:\mBbbN{}n.    \mexists{}n@0:\mBbbN{}.  ((a2\^{}n@0  x)  =  y)
11.  (rotate-by(n;n  -  1)  o  (a1  o  rotate-by(n;1)))  =  (rotate-by(n;n  -  1)  o  (a2  o  rotate-by(n;1)))
12.  (rotate-by(n;1)  o  ((rotate-by(n;n  -  1)  o  (a1  o  rotate-by(n;1)))  o  rotate-by(n;n  -  1)))
=  (rotate-by(n;1)  o  ((rotate-by(n;n  -  1)  o  (a2  o  rotate-by(n;1)))  o  rotate-by(n;n  -  1)))
\mvdash{}  a1  =  a2


By

---

Latex:
((Ext  THEN  Auto)  THEN  ApFunToHypEquands  `Z'  \mkleeneopen{}Z  x\mkleeneclose{}  \mkleeneopen{}\mBbbN{}n\mkleeneclose{}  (-2)\mcdot{}  THEN  Reduce  (-1)  THEN  Auto)

---

Home Index