---

Step * of Lemma p-adics-equal

∀p:ℕ+. ∀x,y:p-adics(p).  uiff(x = y ∈ p-adics(p);∀n:ℕ+. ((x n) ≡ (y n) mod p^n))
BY
{ (Intros
   THEN RepeatFor 2 (D 0)
   THEN Auto
   THEN Try (((RWO "equal-p-adics" (-2) THENA Auto) THEN BLemma `eqmod_weakening` THEN Auto))) }

1
1. p : ℕ+
2. x : p-adics(p)
3. y : p-adics(p)
4. ∀n:ℕ+. ((x n) ≡ (y n) mod p^n)
⊢ x = y ∈ p-adics(p)

---

Latex:

---

Latex:
\mforall{}p:\mBbbN{}\msupplus{}.  \mforall{}x,y:p-adics(p).    uiff(x  =  y;\mforall{}n:\mBbbN{}\msupplus{}.  ((x  n)  \mequiv{}  (y  n)  mod  p\^{}n))


By

---

Latex:
(Intros
  THEN  RepeatFor  2  (D  0)
  THEN  Auto
  THEN  Try  (((RWO  "equal-p-adics"  (-2)  THENA  Auto)  THEN  BLemma  `eqmod\_weakening`  THEN  Auto)))

---

Home Index