---

Step * 1 1 of Lemma pa-inv_wf


1. p : {p:{2...}| prime(p)} 
2. n : ℕ
3. x1 : p-adics(p)
4. p-sep(x1;0(p))
⊢ pa-inv(p;<0, x1>) ∈ {y:padic(p)| pa-mul(p;<0, x1>;y) = 1(p) ∈ padic(p)} 
BY
{ (ThinVar `n'
   THEN (D -1 THEN RepUR ``p-int p-reduce`` -1 THEN (RWO "modulus_base" (-1) THENA Auto))
   THEN RepUR ``pa-inv`` 0) }

1
1. p : {p:{2...}| prime(p)} 
2. x1 : p-adics(p)
3. n : ℕ+
4. ¬((x1 n) = 0 ∈ ℤ)
⊢ eval k = mu(λi.(¬b(x1 (i + 1) =z 0))) in
  let j,b = p-unitize(p;x1;k + 1) 
  in <j, p-inv(p;b)> ∈ {y:padic(p)| pa-mul(p;<0, x1>;y) = 1(p) ∈ padic(p)} 

---

Latex:

---

Latex:

1.  p  :  \{p:\{2...\}|  prime(p)\} 
2.  n  :  \mBbbN{}
3.  x1  :  p-adics(p)
4.  p-sep(x1;0(p))
\mvdash{}  pa-inv(p;ɘ,  x1>)  \mmember{}  \{y:padic(p)|  pa-mul(p;ɘ,  x1>y)  =  1(p)\} 


By

---

Latex:
(ThinVar  `n'
  THEN  (D  -1  THEN  RepUR  ``p-int  p-reduce``  -1  THEN  (RWO  "modulus\_base"  (-1)  THENA  Auto))
  THEN  RepUR  ``pa-inv``  0)

---

Home Index