---

Step * 1 1 1 1 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 ∈ ℤ)
5. k : ℕ
6. (↑¬b(x1 (k + 1) =z 0)) ∧ (∀[i:ℕ]. ¬↑¬b(x1 (i + 1) =z 0) supposing i < k)
7. k1 : ℕ(k + 1) + 1
8. v1 : p-units(p)
9. p^k1(p) * v1 = x1 ∈ p-adics(p)
10. v : p-adics(p)
11. v1 * v = 1(p) ∈ p-adics(p)
⊢ <k1, v> ∈ {y:padic(p)| pa-mul(p;<0, x1>;y) = 1(p) ∈ padic(p)} 
BY
{ Assert ⌜v ∈ p-units(p)⌝⋅ }

1
.....assertion..... 
1. p : {p:{2...}| prime(p)} 
2. x1 : p-adics(p)
3. n : ℕ+
4. ¬((x1 n) = 0 ∈ ℤ)
5. k : ℕ
6. (↑¬b(x1 (k + 1) =z 0)) ∧ (∀[i:ℕ]. ¬↑¬b(x1 (i + 1) =z 0) supposing i < k)
7. k1 : ℕ(k + 1) + 1
8. v1 : p-units(p)
9. p^k1(p) * v1 = x1 ∈ p-adics(p)
10. v : p-adics(p)
11. v1 * v = 1(p) ∈ p-adics(p)
⊢ v ∈ p-units(p)

2
1. p : {p:{2...}| prime(p)} 
2. x1 : p-adics(p)
3. n : ℕ+
4. ¬((x1 n) = 0 ∈ ℤ)
5. k : ℕ
6. (↑¬b(x1 (k + 1) =z 0)) ∧ (∀[i:ℕ]. ¬↑¬b(x1 (i + 1) =z 0) supposing i < k)
7. k1 : ℕ(k + 1) + 1
8. v1 : p-units(p)
9. p^k1(p) * v1 = x1 ∈ p-adics(p)
10. v : p-adics(p)
11. v1 * v = 1(p) ∈ p-adics(p)
12. v ∈ p-units(p)
⊢ <k1, v> ∈ {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)
5.  k  :  \mBbbN{}
6.  (\muparrow{}\mneg{}\msubb{}(x1  (k  +  1)  =\msubz{}  0))  \mwedge{}  (\mforall{}[i:\mBbbN{}].  \mneg{}\muparrow{}\mneg{}\msubb{}(x1  (i  +  1)  =\msubz{}  0)  supposing  i  <  k)
7.  k1  :  \mBbbN{}(k  +  1)  +  1
8.  v1  :  p-units(p)
9.  p\^{}k1(p)  *  v1  =  x1
10.  v  :  p-adics(p)
11.  v1  *  v  =  1(p)
\mvdash{}  <k1,  v>  \mmember{}  \{y:padic(p)|  pa-mul(p;ɘ,  x1>y)  =  1(p)\} 


By

---

Latex:
Assert  \mkleeneopen{}v  \mmember{}  p-units(p)\mkleeneclose{}\mcdot{}

---

Home Index