---

Step * of Lemma p-sep-or

∀[p:ℕ+]. ∀[x:p-adics(p)].  ∀y:p-adics(p). (p-sep(x;y) ⇒ (∀z:p-adics(p). (p-sep(z;x) ∨ p-sep(z;y))))
BY
{ (Auto THEN D -2 THEN (Decide ⌜(z n) = (y n) ∈ ℤ⌝⋅ THENA Auto)) }

1
1. [p] : ℕ+
2. [x] : p-adics(p)
3. y : p-adics(p)
4. n : ℕ+
5. ¬((x n) = (y n) ∈ ℤ)
6. z : p-adics(p)
7. (z n) = (y n) ∈ ℤ
⊢ p-sep(z;x) ∨ p-sep(z;y)

2
1. [p] : ℕ+
2. [x] : p-adics(p)
3. y : p-adics(p)
4. n : ℕ+
5. ¬((x n) = (y n) ∈ ℤ)
6. z : p-adics(p)
7. ¬((z n) = (y n) ∈ ℤ)
⊢ p-sep(z;x) ∨ p-sep(z;y)

---

Latex:

---

Latex:
\mforall{}[p:\mBbbN{}\msupplus{}].  \mforall{}[x:p-adics(p)].    \mforall{}y:p-adics(p).  (p-sep(x;y)  {}\mRightarrow{}  (\mforall{}z:p-adics(p).  (p-sep(z;x)  \mvee{}  p-sep(z;y))))


By

---

Latex:
(Auto  THEN  D  -2  THEN  (Decide  \mkleeneopen{}(z  n)  =  (y  n)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index