---

Step * of Lemma p-adic-inv-lemma

∀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
{ Extract of Obid: p-adic-inv-lemma1
  not unfolding  sign absval exp remainder
  finishing with Auto
  normalizes to:
  
  λp,a,n. let x,y = letrec rec(p)=λq.if p=0
                                     then <q, 0, 1, 1, 1, Ax, Ax, Ax>
                                     else let x,y = divrem(q; p) 
                                          in eval r = y in
                                             let g,t = rec r p 
                                             in let a,b,x1,y1,_,_,_@0 = t in 
                                                 eval q' = x in
                                                 eval b' = (b * q') + a in
                                                 eval x' = y1 - x1 * q' in
                                                   <g, b, b', x', x1, Ax, Ax, Ax> in
                     rec(|a n|) 
                    |p^n| 
          in let x1,x2,x3,x4,x5,x5,y = y in 
              eval r = sign(a n) * x3 rem p^n in
              if (r) < (0)  then |p^n| + r  else r }

---

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:
Extract  of  Obid:  p-adic-inv-lemma1
not  unfolding    sign  absval  exp  remainder
finishing  with  Auto
normalizes  to:

\mlambda{}p,a,n.  let  x,y  =  letrec  rec(p)=\mlambda{}q.if  p=0
                                                                      then  <q,  0,  1,  1,  1,  Ax,  Ax,  Ax>
                                                                      else  let  x,y  =  divrem(q;  p) 
                                                                                in  eval  r  =  y  in
                                                                                      let  g,t  =  rec  r  p 
                                                                                      in  let  a,b,x1,y1,$_{}$,$_\mbackslash{}ff7\000Cb}$,$_{@0}$  =  t  in 
                                                                                              eval  q'  =  x  in
                                                                                              eval  b'  =  (b  *  q')  +  a  in
                                                                                              eval  x'  =  y1  -  x1  *  q'  in
                                                                                                  <g,  b,  b',  x',  x1,  Ax,  Ax,  Ax>  in
                                      rec(|a  n|) 
                                    |p\^{}n| 
                in  let  x1,x2,x3,x4,x5,x5,y  =  y  in 
                        eval  r  =  sign(a  n)  *  x3  rem  p\^{}n  in
                        if  (r)  <  (0)    then  |p\^{}n|  +  r    else  r

---

Home Index