---

Step * 2 1 1 1 1 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)
7. v : p-adics(p)
8. u * v = 1(p) ∈ p-adics(p)
⊢ 1(p) * u * p^n(p) * v = p^n(p) * 1(p) ∈ p-adics(p)
BY
{ ((RWW "p-1-mul p-mul-1" 0 THENA Auto)
   THEN (RW (AddrC [2;3] (LemmaC `p-mul-comm`)) 0  THENA Auto)
   THEN (RWO "p-mul-assoc" 0 THENA Auto)
   THEN RWW "-1 p-mul-1" 0
   THEN Auto) }

---

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
7.  v  :  p-adics(p)
8.  u  *  v  =  1(p)
\mvdash{}  1(p)  *  u  *  p\^{}n(p)  *  v  =  p\^{}n(p)  *  1(p)


By

---

Latex:
((RWW  "p-1-mul  p-mul-1"  0  THENA  Auto)
  THEN  (RW  (AddrC  [2;3]  (LemmaC  `p-mul-comm`))  0    THENA  Auto)
  THEN  (RWO  "p-mul-assoc"  0  THENA  Auto)
  THEN  RWW  "-1  p-mul-1"  0
  THEN  Auto)

---

Home Index