---

Step * of Lemma p-adic-inv-lemma1

∀p:{p:{2...}| prime(p)} . ∀a:{a:p-adics(p)| ¬((a 1) = 0 ∈ ℤ)} . ∀n:ℕ+.  (∃c:ℕp^n [((c * (a n)) ≡ 1 mod p^n)])
BY
{ (Auto THEN (InstLemma `p-adic-property` [⌜p⌝;⌜a⌝;⌜1⌝;⌜n⌝]⋅ THENA Auto) THEN Subst' p^1 ~ p -1 THEN Auto) }

1
1. p : {p:{2...}| prime(p)} 
2. a : {a:p-adics(p)| ¬((a 1) = 0 ∈ ℤ)} 
3. n : ℕ+
4. (a n) ≡ (a 1) mod p
⊢ ∃c:ℕp^n [((c * (a n)) ≡ 1 mod p^n)]

---

Latex:

---

Latex:
\mforall{}p:\{p:\{2...\}|  prime(p)\}  .  \mforall{}a:\{a:p-adics(p)|  \mneg{}((a  1)  =  0)\}  .  \mforall{}n:\mBbbN{}\msupplus{}.
    (\mexists{}c:\mBbbN{}p\^{}n  [((c  *  (a  n))  \mequiv{}  1  mod  p\^{}n)])


By

---

Latex:
(Auto
  THEN  (InstLemma  `p-adic-property`  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Subst'  p\^{}1  \msim{}  p  -1
  THEN  Auto)

---

Home Index