---

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

∀[p:{2...}]. ∀[k:ℕ]. ∀[a,b:p-adics(p)].  ((p^k(p) * a = p^k(p) * b ∈ p-adics(p)) ⇒ (a = b ∈ p-adics(p)))
BY
{ (Auto
   THEN DupHyp (-1)
   THEN (RWO "p-adics-equal" (-1) THENA Auto)
   THEN RWO "p-adics-equal" 0 
   THEN Auto
   THEN RepUR ``p-mul p-int`` -2
   THEN (RWW "p-reduce-eqmod" (-2) THENA Auto)) }

1
1. p : {2...}
2. k : ℕ
3. a : p-adics(p)
4. b : p-adics(p)
5. p^k(p) * a = p^k(p) * b ∈ p-adics(p)
6. ∀n:ℕ+. ((p^k * (a n)) ≡ (p^k * (b n)) mod p^n)
7. n : ℕ+
⊢ (a n) ≡ (b n) mod p^n

---

Latex:

---

Latex:
\mforall{}[p:\{2...\}].  \mforall{}[k:\mBbbN{}].  \mforall{}[a,b:p-adics(p)].    ((p\^{}k(p)  *  a  =  p\^{}k(p)  *  b)  {}\mRightarrow{}  (a  =  b))


By

---

Latex:
(Auto
  THEN  DupHyp  (-1)
  THEN  (RWO  "p-adics-equal"  (-1)  THENA  Auto)
  THEN  RWO  "p-adics-equal"  0 
  THEN  Auto
  THEN  RepUR  ``p-mul  p-int``  -2
  THEN  (RWW  "p-reduce-eqmod"  (-2)  THENA  Auto))

---

Home Index