---

Step * 1 of Lemma pa-inv_wf


1. p : {p:{2...}| prime(p)} 
2. n : ℕ
3. x1 : if (n =z 0) then p-adics(p) else p-units(p) fi 
4. (¬(n = 0 ∈ ℤ)) ∨ p-sep(x1;0(p))
5. n = 0 ∈ ℤ
⊢ pa-inv(p;<0, x1>) ∈ {y:padic(p)| pa-mul(p;<0, x1>;y) = 1(p) ∈ padic(p)} 
BY
{ (Eliminate ⌜n⌝⋅ THEN Thin (-1) THEN D -1 THEN Try ((D -1 THEN Fold `member` 0 THEN Auto)) THEN Reduce -2) }

1
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)} 

---

Latex:

---

Latex:

1.  p  :  \{p:\{2...\}|  prime(p)\} 
2.  n  :  \mBbbN{}
3.  x1  :  if  (n  =\msubz{}  0)  then  p-adics(p)  else  p-units(p)  fi 
4.  (\mneg{}(n  =  0))  \mvee{}  p-sep(x1;0(p))
5.  n  =  0
\mvdash{}  pa-inv(p;ɘ,  x1>)  \mmember{}  \{y:padic(p)|  pa-mul(p;ɘ,  x1>y)  =  1(p)\} 


By

---

Latex:
(Eliminate  \mkleeneopen{}n\mkleeneclose{}\mcdot{}
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  Try  ((D  -1  THEN  Fold  `member`  0  THEN  Auto))
  THEN  Reduce  -2)

---

Home Index