---

Step * 2 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 ∈ ℤ)
5. u : p-units(p)
6. x1 = u ∈ p-units(p)
⊢ <0, p^n(p) * p-inv(p;u)> ∈ {y:padic(p)| pa-mul(p;<n, u>;y) = 1(p) ∈ padic(p)} 
BY
{ ((GenConclTerm ⌜p-inv(p;u)⌝⋅ THENA Auto) THEN Thin (-1) THEN D -1) }

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 ∈ ℤ)
5. u : p-units(p)
6. x1 = u ∈ p-units(p)
7. v : p-adics(p)
8. u * v = 1(p) ∈ p-adics(p)
⊢ <0, p^n(p) * v> ∈ {y:padic(p)| pa-mul(p;<n, u>;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)
5.  u  :  p-units(p)
6.  x1  =  u
\mvdash{}  ɘ,  p\^{}n(p)  *  p-inv(p;u)>  \mmember{}  \{y:padic(p)|  pa-mul(p;<n,  u>y)  =  1(p)\} 


By

---

Latex:
((GenConclTerm  \mkleeneopen{}p-inv(p;u)\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  Thin  (-1)  THEN  D  -1)

---

Home Index