---

Step * 1 1 2 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))
∧ (∀b:ℕn. ((rotate-by(n;n - 1) (rotate-by(n;1) b)) = b ∈ ℕn))
⊢ (n - 1)! ≡ (n - 1) mod n
BY
{ (D (-1)
   THEN (BLemma `eqmod-prime-order-fixedpoints` THEN Auto)
   THEN (InstConcl [⌜cyclic-map(ℕn)⌝;⌜λf.(rotate-by(n;n - 1) o (f o rotate-by(n;1)))⌝]⋅
         THENA (Auto THEN BLemma `cyclic-map-conjugate` THEN Auto)
         )
   THEN Reduce 0
   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)!
⊢ Inj(cyclic-map(ℕn);cyclic-map(ℕn);λf.(rotate-by(n;n - 1) o (f o rotate-by(n;1))))

2
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))))
⊢ {x:cyclic-map(ℕn)| (rotate-by(n;n - 1) o (x o rotate-by(n;1))) = x ∈ cyclic-map(ℕn)}  ~ ℕn - 1

3
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. {x:cyclic-map(ℕn)| (rotate-by(n;n - 1) o (x o rotate-by(n;1))) = x ∈ cyclic-map(ℕn)}  ~ ℕn - 1
8. x : cyclic-map(ℕn)
⊢ (λf.(rotate-by(n;n - 1) o (f o rotate-by(n;1)))^n x) = x ∈ cyclic-map(ℕ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))
\mwedge{}  (\mforall{}b:\mBbbN{}n.  ((rotate-by(n;n  -  1)  (rotate-by(n;1)  b))  =  b))
\mvdash{}  (n  -  1)!  \mequiv{}  (n  -  1)  mod  n


By

---

Latex:
(D  (-1)
  THEN  (BLemma  `eqmod-prime-order-fixedpoints`  THEN  Auto)
  THEN  (InstConcl  [\mkleeneopen{}cyclic-map(\mBbbN{}n)\mkleeneclose{};\mkleeneopen{}\mlambda{}f.(rotate-by(n;n  -  1)  o  (f  o  rotate-by(n;1)))\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  BLemma  `cyclic-map-conjugate`  THEN  Auto)
              )
  THEN  Reduce  0
  THEN  Auto)

---

Home Index