---

Step * 1 1 1 of Lemma pa-inv_wf


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)} 
BY
{ ((InstLemma `mu_wf` [⌜λi.(¬b(x1 (i + 1) =z 0))⌝]⋅ THENA (Auto THEN Reduce 0 THEN D 0 With ⌜n - 1⌝  THEN Auto))
   THEN (InstLemma `mu-property` [⌜λi.(¬b(x1 (i + 1) =z 0))⌝]⋅
         THENA (Auto THEN Reduce 0 THEN D 0 With ⌜n - 1⌝  THEN Auto)
         )
   THEN Reduce -1
   THEN MoveToConcl  (-1)
   THEN (GenConclTerm ⌜mu(λi.(¬b(x1 (i + 1) =z 0)))⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN Thin (-2)
   THEN RenameVar `k' (-1)) }

1
1. p : {p:{2...}| prime(p)} 
2. x1 : p-adics(p)
3. n : ℕ+
4. ¬((x1 n) = 0 ∈ ℤ)
5. k : ℕ
⊢ ((↑¬b(x1 (k + 1) =z 0)) ∧ (∀[i:ℕ]. ¬↑¬b(x1 (i + 1) =z 0) supposing i < k))
⇒ (eval k = k 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.  x1  :  p-adics(p)
3.  n  :  \mBbbN{}\msupplus{}
4.  \mneg{}((x1  n)  =  0)
\mvdash{}  eval  k  =  mu(\mlambda{}i.(\mneg{}\msubb{}(x1  (i  +  1)  =\msubz{}  0)))  in
    let  j,b  =  p-unitize(p;x1;k  +  1) 
    in  <j,  p-inv(p;b)>  \mmember{}  \{y:padic(p)|  pa-mul(p;ɘ,  x1>y)  =  1(p)\} 


By

---

Latex:
((InstLemma  `mu\_wf`  [\mkleeneopen{}\mlambda{}i.(\mneg{}\msubb{}(x1  (i  +  1)  =\msubz{}  0))\mkleeneclose{}]\mcdot{}
    THENA  (Auto  THEN  Reduce  0  THEN  D  0  With  \mkleeneopen{}n  -  1\mkleeneclose{}    THEN  Auto)
    )
  THEN  (InstLemma  `mu-property`  [\mkleeneopen{}\mlambda{}i.(\mneg{}\msubb{}(x1  (i  +  1)  =\msubz{}  0))\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  Reduce  0  THEN  D  0  With  \mkleeneopen{}n  -  1\mkleeneclose{}    THEN  Auto)
              )
  THEN  Reduce  -1
  THEN  MoveToConcl    (-1)
  THEN  (GenConclTerm  \mkleeneopen{}mu(\mlambda{}i.(\mneg{}\msubb{}(x1  (i  +  1)  =\msubz{}  0)))\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  Thin  (-2)
  THEN  RenameVar  `k'  (-1))

---

Home Index