---

Step * 1 1 2 2 1 1 1 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 : ℕ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
11. i : ℤ
12. 0 < i
13. i < n
14. (f ((-i) + n)) = ((-i) + n + (f 0) rem n) ∈ ℤ
15. 0 ≤ f (n - i + 1) < n
⊢ (((-i) + n + (f 0) rem n) + (n - 1) rem n) = ((n - i + 1) + (f 0) rem n) ∈ ℤ
BY
{ ((InstLemma `rem_addition` [⌜(-i) + n + (f 0)⌝;⌜n - 1⌝;⌜n⌝]⋅ THENA Auto') THEN NthHypEq (-1) THEN EqCD 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. 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
11. i : ℤ
12. 0 < i
13. i < n
14. (f ((-i) + n)) = ((-i) + n + (f 0) rem n) ∈ ℤ
15. 0 ≤ (f (n - i + 1))
16. f (n - i + 1) < n
17. (((-i) + n + (f 0) rem n) + (n - 1 rem n) rem n) = (((-i) + n + (f 0)) + (n - 1) rem n) ∈ ℤ
⊢ ((n - i + 1) + (f 0) rem n) = (((-i) + n + (f 0)) + (n - 1) rem 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.  Inj(cyclic-map(\mBbbN{}n);cyclic-map(\mBbbN{}n);\mlambda{}f.(rotate-by(n;n  -  1)  o  (f  o  rotate-by(n;1))))
7.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n
8.  (rotate-by(n;n  -  1)  o  (f  o  rotate-by(n;1)))  =  f
9.  \mforall{}x:\mBbbN{}n.  ((f  x)  =  ((f  (x  +  1  rem  n))  +  (n  -  1)  rem  n))
10.  x  :  \mBbbN{}n
11.  i  :  \mBbbZ{}
12.  0  <  i
13.  i  <  n
14.  (f  ((-i)  +  n))  =  ((-i)  +  n  +  (f  0)  rem  n)
15.  0  \mleq{}  f  (n  -  i  +  1)  <  n
\mvdash{}  (((-i)  +  n  +  (f  0)  rem  n)  +  (n  -  1)  rem  n)  =  ((n  -  i  +  1)  +  (f  0)  rem  n)


By

---

Latex:
((InstLemma  `rem\_addition`  [\mkleeneopen{}(-i)  +  n  +  (f  0)\mkleeneclose{};\mkleeneopen{}n  -  1\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto')
  THEN  NthHypEq  (-1)
  THEN  EqCD
  THEN  Auto)

---

Home Index