---

Step * of Lemma pa-inv_wf

∀p:{p:{2...}| prime(p)} . ∀x:{x:padic(p)| pa-sep(p;x;0(p))} .
  (pa-inv(p;x) ∈ {y:padic(p)| pa-mul(p;x;y) = 1(p) ∈ padic(p)} )
BY
{ (Intros THEN D -1 THEN D -2 THEN RepUR ``pa-sep pa-int`` -1 THEN CaseNat 0 `n') }

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

2
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;<n, x1>) ∈ {y:padic(p)| pa-mul(p;<n, x1>;y) = 1(p) ∈ padic(p)} 

---

Latex:

---

Latex:
\mforall{}p:\{p:\{2...\}|  prime(p)\}  .  \mforall{}x:\{x:padic(p)|  pa-sep(p;x;0(p))\}  .
    (pa-inv(p;x)  \mmember{}  \{y:padic(p)|  pa-mul(p;x;y)  =  1(p)\}  )


By

---

Latex:
(Intros  THEN  D  -1  THEN  D  -2  THEN  RepUR  ``pa-sep  pa-int``  -1  THEN  CaseNat  0  `n')

---

Home Index