---

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

.....assertion..... 
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. Inj(cyclic-map(ℕn);cyclic-map(ℕn);λf.(rotate-by(n;n - 1) o (f o rotate-by(n;1))))
⊢ ∀f:{x:ℕn ⟶ ℕn| (rotate-by(n;n - 1) o (x o rotate-by(n;1))) = x ∈ (ℕn ⟶ ℕn)} . (f = rotate-by(n;f 0) ∈ (ℕn ⟶ ℕn))
BY
{ ((Auto THEN D -1)
   THEN (Assert ∀x:ℕn. ((f x) = ((rotate-by(n;n - 1) o (f o rotate-by(n;1))) x) ∈ ℕn) BY
               Auto)
   THEN RepUR ``rotate-by`` -1
   THEN Ext
   THEN Reduce 0
   THEN Auto
   THEN TACTIC:((EqTypeCD THEN Auto') THEN Unfold `rotate-by` 0 THEN Reduce 0)) }

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. Inj(cyclic-map(ℕn);cyclic-map(ℕn);λf.(rotate-by(n;n - 1) o (f o rotate-by(n;1))))
7. f : ℕn ⟶ ℕn
8. (rotate-by(n;n - 1) o (f o rotate-by(n;1))) = f ∈ (ℕn ⟶ ℕn)
9. ∀x:ℕn. ((f x) = ((f (x + 1 rem n)) + (n - 1) rem n) ∈ ℕn)
10. x : ℕn
⊢ (f x) = (x + (f 0) rem n) ∈ ℤ

---

Latex:

---

Latex:
.....assertion..... 
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.  Inj(cyclic-map(\mBbbN{}n);cyclic-map(\mBbbN{}n);\mlambda{}f.(rotate-by(n;n  -  1)  o  (f  o  rotate-by(n;1))))
\mvdash{}  \mforall{}f:\{x:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  (rotate-by(n;n  -  1)  o  (x  o  rotate-by(n;1)))  =  x\}  .  (f  =  rotate-by(n;f  0))


By

---

Latex:
((Auto  THEN  D  -1)
  THEN  (Assert  \mforall{}x:\mBbbN{}n.  ((f  x)  =  ((rotate-by(n;n  -  1)  o  (f  o  rotate-by(n;1)))  x))  BY
                          Auto)
  THEN  RepUR  ``rotate-by``  -1
  THEN  Ext
  THEN  Reduce  0
  THEN  Auto
  THEN  TACTIC:((EqTypeCD  THEN  Auto')  THEN  Unfold  `rotate-by`  0  THEN  Reduce  0))

---

Home Index