---

Step * 1 1 of Lemma eqmod-prime-order-fixedpoints


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)
16. ||L|| | p
⊢ (||L|| = 1 ∈ ℤ) ∨ (p | ||L||)
BY
{ ((FLemma `divides-prime` [-1] THENA Auto) THEN D -1) }

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)
16. ||L|| | p
17. ||L|| ~ p
⊢ (||L|| = 1 ∈ ℤ) ∨ (p | ||L||)

2
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)
16. ||L|| | p
17. (||L|| ~ 1) ∨ (||L|| = 0 ∈ ℤ)
⊢ (||L|| = 1 ∈ ℤ) ∨ (p | ||L||)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  k  :  \mBbbN{}
3.  p  :  \mBbbN{}
4.  prime(p)
5.  T  :  Type
6.  f  :  T  {}\mrightarrow{}  T
7.  T  \msim{}  \mBbbN{}n
8.  Inj(T;T;f)
9.  \{x:T|  (f  x)  =  x\}    \msim{}  \mBbbN{}k
10.  \mforall{}x:T.  ((f\^{}p  x)  =  x)
11.  T  \msim{}  \mBbbN{}n
12.  Inj(T;T;f)
13.  \{x:T|  (f  x)  =  x\}    \msim{}  \mBbbN{}k
14.  L  :  T  List
15.  orbit(T;f;L)
16.  ||L||  |  p
\mvdash{}  (||L||  =  1)  \mvee{}  (p  |  ||L||)


By

---

Latex:
((FLemma  `divides-prime`  [-1]  THENA  Auto)  THEN  D  -1)

---

Home Index