---

Step * 1 1 2 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 : 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)
BY
{ (DVar `a1' THEN DVar `a2' THEN EqTypeCD THEN Try (Complete (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. ∀x,y:ℕn.  ∃n@0:ℕ. ((a1^n@0 x) = y ∈ ℕn)
8. a2 : ℕn →⟶ ℕn
9. ∀x,y:ℕn.  ∃n@0:ℕ. ((a2^n@0 x) = y ∈ ℕn)
10. (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)
11. (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

---

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  :  cyclic-map(\mBbbN{}n)
7.  a2  :  cyclic-map(\mBbbN{}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)))
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)))
\mvdash{}  a1  =  a2


By

---

Latex:
(DVar  `a1'  THEN  DVar  `a2'  THEN  EqTypeCD  THEN  Try  (Complete  (Auto)))

---

Home Index