---

Step * 1 1 2 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)!
⊢ Inj(cyclic-map(ℕn);cyclic-map(ℕn);λf.(rotate-by(n;n - 1) o (f o rotate-by(n;1))))
BY
{ (D 0
   THEN Reduce 0
   THEN Auto
   THEN Try ((BLemma `cyclic-map-conjugate` THEN Auto))
   THEN ApFunToHypEquands `Z' ⌜rotate-by(n;1) o (Z o rotate-by(n;n - 1))⌝ ⌜cyclic-map(ℕn)⌝ (-1)⋅
   THEN Auto
   THEN Try ((BLemma `cyclic-map-conjugate` 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 : cyclic-map(ℕn)
7. a2 : cyclic-map(ℕn)
8. (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)
9. (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 ∈ cyclic-map(ℕ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)!
\mvdash{}  Inj(cyclic-map(\mBbbN{}n);cyclic-map(\mBbbN{}n);\mlambda{}f.(rotate-by(n;n  -  1)  o  (f  o  rotate-by(n;1))))


By

---

Latex:
(D  0
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  ((BLemma  `cyclic-map-conjugate`  THEN  Auto))
  THEN  ApFunToHypEquands  `Z'  \mkleeneopen{}rotate-by(n;1)  o  (Z  o  rotate-by(n;n  -  1))\mkleeneclose{}  \mkleeneopen{}cyclic-map(\mBbbN{}n)\mkleeneclose{}  (-1)\mcdot{}
  THEN  Auto
  THEN  Try  ((BLemma  `cyclic-map-conjugate`  THEN  Auto)))\mcdot{}

---

Home Index