---

Step * 1 1 2 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. ∀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
BY
{ (DVar `a1' THEN EqTypeCD 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)
⊢ 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  :  \mBbbN{}n  \mrightarrow{}{}\mrightarrow{}  \mBbbN{}n
7.  \mforall{}x,y:\mBbbN{}n.    \mexists{}n@0:\mBbbN{}.  ((a1\^{}n@0  x)  =  y)
8.  a2  :  \mBbbN{}n  \mrightarrow{}{}\mrightarrow{}  \mBbbN{}n
9.  \mforall{}x,y:\mBbbN{}n.    \mexists{}n@0:\mBbbN{}.  ((a2\^{}n@0  x)  =  y)
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)))
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)))
\mvdash{}  a1  =  a2


By

---

Latex:
(DVar  `a1'  THEN  EqTypeCD  THEN  Auto)

---

Home Index