---

Step * of Lemma eqmod-prime-order-fixedpoints

∀n,k,p:ℕ.
  (prime(p)
  ⇒ (∃T:Type. ∃f:T ⟶ T. (T ~ ℕn ∧ Inj(T;T;f) ∧ {x:T| (f x) = x ∈ T}  ~ ℕk ∧ (∀x:T. ((f^p x) = x ∈ T))))
  ⇒ (n ≡ k mod p))
BY
{ (Auto THEN BLemma `eqmod-by-orbits` THEN Auto THEN RepeatFor 2 (ParallelLast) THEN Auto) }

1
1. n : ℕ
2. k : ℕ
3. p : ℕ
4. prime(p)
5. T : Type
6. f : T ⟶ T
7. T ~ ℕn
8. Inj(T;T;f)
9. {x:T| (f x) = x ∈ T}  ~ ℕk
10. ∀x:T. ((f^p x) = x ∈ T)
11. T ~ ℕn
12. Inj(T;T;f)
13. {x:T| (f x) = x ∈ T}  ~ ℕk
14. L : T List
15. orbit(T;f;L)
⊢ (||L|| = 1 ∈ ℤ) ∨ (p | ||L||)

---

Latex:

---

Latex:
\mforall{}n,k,p:\mBbbN{}.
    (prime(p)
    {}\mRightarrow{}  (\mexists{}T:Type.  \mexists{}f:T  {}\mrightarrow{}  T.  (T  \msim{}  \mBbbN{}n  \mwedge{}  Inj(T;T;f)  \mwedge{}  \{x:T|  (f  x)  =  x\}    \msim{}  \mBbbN{}k  \mwedge{}  (\mforall{}x:T.  ((f\^{}p  x)  =  x))))
    {}\mRightarrow{}  (n  \mequiv{}  k  mod  p))


By

---

Latex:
(Auto  THEN  BLemma  `eqmod-by-orbits`  THEN  Auto  THEN  RepeatFor  2  (ParallelLast)  THEN  Auto)

---

Home Index