---

Step * of Lemma p-sep-irrefl

∀[p:ℕ+]. ∀[x:p-adics(p)].  (¬p-sep(x;x))
BY
{ (Auto THEN (D 0 THENA Auto) THEN RepeatFor 2 (D -1)) }

1
1. p : ℕ+
2. x : p-adics(p)
3. n : ℕ+
⊢ (x n) = (x n) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[p:\mBbbN{}\msupplus{}].  \mforall{}[x:p-adics(p)].    (\mneg{}p-sep(x;x))


By

---

Latex:
(Auto  THEN  (D  0  THENA  Auto)  THEN  RepeatFor  2  (D  -1))

---

Home Index