---

Step * 1 1 2 2 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. Inj(cyclic-map(ℕn);cyclic-map(ℕn);λf.(rotate-by(n;n - 1) o (f o rotate-by(n;1))))
7. ∀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))
8. f : ℕn →⟶ ℕn
9. ∀x,y:ℕn.  ∃n@0:ℕ. ((f^n@0 x) = y ∈ ℕn)
10. (rotate-by(n;n - 1) o (f o rotate-by(n;1))) = f ∈ (ℕn ⟶ ℕn)
11. (f 0) = 0 ∈ ℤ
12. f = rotate-by(n;0) ∈ (ℕn ⟶ ℕn)
⊢ False
BY
{ ((Assert 0 ∈ ℕn BY Auto) THEN (Assert 1 ∈ ℕn BY Auto) THEN (InstHyp [⌜0⌝;⌜1⌝] (-6)⋅ THENA 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. Inj(cyclic-map(ℕn);cyclic-map(ℕn);λf.(rotate-by(n;n - 1) o (f o rotate-by(n;1))))
7. ∀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))
8. f : ℕn →⟶ ℕn
9. ∀x,y:ℕn.  ∃n@0:ℕ. ((f^n@0 x) = y ∈ ℕn)
10. (rotate-by(n;n - 1) o (f o rotate-by(n;1))) = f ∈ (ℕn ⟶ ℕn)
11. (f 0) = 0 ∈ ℤ
12. f = rotate-by(n;0) ∈ (ℕn ⟶ ℕn)
13. 0 ∈ ℕn
14. 1 ∈ ℕn
15. ∃n@0:ℕ. ((f^n@0 0) = 1 ∈ ℕn)
⊢ False

---

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.  Inj(cyclic-map(\mBbbN{}n);cyclic-map(\mBbbN{}n);\mlambda{}f.(rotate-by(n;n  -  1)  o  (f  o  rotate-by(n;1))))
7.  \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))
8.  f  :  \mBbbN{}n  \mrightarrow{}{}\mrightarrow{}  \mBbbN{}n
9.  \mforall{}x,y:\mBbbN{}n.    \mexists{}n@0:\mBbbN{}.  ((f\^{}n@0  x)  =  y)
10.  (rotate-by(n;n  -  1)  o  (f  o  rotate-by(n;1)))  =  f
11.  (f  0)  =  0
12.  f  =  rotate-by(n;0)
\mvdash{}  False


By

---

Latex:
((Assert  0  \mmember{}  \mBbbN{}n  BY  Auto)  THEN  (Assert  1  \mmember{}  \mBbbN{}n  BY  Auto)  THEN  (InstHyp  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{}]  (-6)\mcdot{}  THENA  Auto))

---

Home Index