---

Step * of Lemma fermat-little2

∀p:ℕ. (prime(p) ⇒ (∀x:ℕ. x^p - 1 ≡ 1 mod p supposing ¬(p | x)))
BY
{ (Auto
   THEN (InstLemma `fermat-little` [⌜p⌝;⌜x⌝]⋅ THENA Auto)
   THEN Using [`x',⌜x⌝] (BLemma `eqmod_cancellation`)⋅
   THEN Auto) }

1
1. p : ℕ@i
2. prime(p)@i
3. x : ℕ@i
4. ¬(p | x)
5. x^p ≡ x mod p
⊢ p - 1 ∈ ℕ

2
1. p : ℕ@i
2. prime(p)@i
3. x : ℕ@i
4. ¬(p | x)
5. x^p ≡ x mod p
⊢ CoPrime(x,p)

3
1. p : ℕ@i
2. prime(p)@i
3. x : ℕ@i
4. ¬(p | x)
5. x^p ≡ x mod p
⊢ (x * x^p - 1) ≡ (x * 1) mod p

---

Latex:

---

Latex:
\mforall{}p:\mBbbN{}.  (prime(p)  {}\mRightarrow{}  (\mforall{}x:\mBbbN{}.  x\^{}p  -  1  \mequiv{}  1  mod  p  supposing  \mneg{}(p  |  x)))


By

---

Latex:
(Auto
  THEN  (InstLemma  `fermat-little`  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Using  [`x',\mkleeneopen{}x\mkleeneclose{}]  (BLemma  `eqmod\_cancellation`)\mcdot{}
  THEN  Auto)

---

Home Index