---

Step * 2 1 1 of Lemma p-inv_wf


1. p : {p:{2...}| prime(p)} 
2. a : p-adics(p)
3. ¬((a 1) = 0 ∈ ℤ)
4. f : n:ℕ+ ⟶ (∃c:ℕp^n [((c * (a n)) ≡ 1 mod p^n)])
5. n : ℕ+
⊢ (f (n + 1)) ≡ (f n) mod p^n
BY
{ (GenConclTerms Auto [⌜f (n + 1)⌝;⌜f n⌝]⋅ THEN ThinVar `f' THEN D -2 THEN D -1) }

1
1. p : {p:{2...}| prime(p)} 
2. a : p-adics(p)
3. ¬((a 1) = 0 ∈ ℤ)
4. n : ℕ+
5. v : ℕp^(n + 1)
6. [%2] : (v * (a (n + 1))) ≡ 1 mod p^(n + 1)
7. v1 : ℕp^n
8. [%3] : (v1 * (a n)) ≡ 1 mod p^n
⊢ v ≡ v1 mod p^n

---

Latex:

---

Latex:

1.  p  :  \{p:\{2...\}|  prime(p)\} 
2.  a  :  p-adics(p)
3.  \mneg{}((a  1)  =  0)
4.  f  :  n:\mBbbN{}\msupplus{}  {}\mrightarrow{}  (\mexists{}c:\mBbbN{}p\^{}n  [((c  *  (a  n))  \mequiv{}  1  mod  p\^{}n)])
5.  n  :  \mBbbN{}\msupplus{}
\mvdash{}  (f  (n  +  1))  \mequiv{}  (f  n)  mod  p\^{}n


By

---

Latex:
(GenConclTerms  Auto  [\mkleeneopen{}f  (n  +  1)\mkleeneclose{};\mkleeneopen{}f  n\mkleeneclose{}]\mcdot{}  THEN  ThinVar  `f'  THEN  D  -2  THEN  D  -1)

---

Home Index