---

Step * of Lemma fermat-little

∀p:ℕ. (prime(p) ⇒ (∀x:ℕ. (x^p ≡ x mod p)))
BY
{ TACTIC:(Auto THEN BLemma `eqmod-prime-order-fixedpoints` THEN Auto) }

1
1. p : ℕ
2. prime(p)
3. x : ℕ
⊢ ∃T:Type. ∃f:T ⟶ T. (T ~ ℕx^p ∧ Inj(T;T;f) ∧ {x:T| (f x) = x ∈ T}  ~ ℕx ∧ (∀x:T. ((f^p x) = x ∈ T)))

---

Latex:

---

Latex:
\mforall{}p:\mBbbN{}.  (prime(p)  {}\mRightarrow{}  (\mforall{}x:\mBbbN{}.  (x\^{}p  \mequiv{}  x  mod  p)))


By

---

Latex:
TACTIC:(Auto  THEN  BLemma  `eqmod-prime-order-fixedpoints`  THEN  Auto)

---

Home Index