---

Step * of Lemma p-mul-int-cancelation-2

∀[p:{p:{2...}| prime(p)} ]. ∀[k:ℕ]. ∀[a,b:p-adics(p)].
  (a = b ∈ p-adics(p)) supposing ((k(p) * a = k(p) * b ∈ p-adics(p)) and CoPrime(k,p))
BY
{ (Auto THEN (InstLemma `p-inv_wf` [⌜p⌝;⌜k(p)⌝]⋅ THENA Auto)) }

1
.....wf..... 
1. p : {p:{2...}| prime(p)} 
2. k : ℕ
3. a : p-adics(p)
4. b : p-adics(p)
5. CoPrime(k,p)
6. k(p) * a = k(p) * b ∈ p-adics(p)
⊢ k(p) ∈ p-units(p)

2
1. p : {p:{2...}| prime(p)} 
2. k : ℕ
3. a : p-adics(p)
4. b : p-adics(p)
5. CoPrime(k,p)
6. k(p) * a = k(p) * b ∈ p-adics(p)
7. p-inv(p;k(p)) ∈ {b:p-adics(p)| k(p) * b = 1(p) ∈ p-adics(p)} 
⊢ a = b ∈ p-adics(p)

---

Latex:

---

Latex:
\mforall{}[p:\{p:\{2...\}|  prime(p)\}  ].  \mforall{}[k:\mBbbN{}].  \mforall{}[a,b:p-adics(p)].
    (a  =  b)  supposing  ((k(p)  *  a  =  k(p)  *  b)  and  CoPrime(k,p))


By

---

Latex:
(Auto  THEN  (InstLemma  `p-inv\_wf`  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}k(p)\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index