---

Step * of Lemma bpa-norm_wf_padic

∀[p:ℕ+]. ∀[x:basic-padic(p)].  (bpa-norm(p;x) ∈ padic(p))
BY
{ ((Intros THEN Unhide) THEN D 2 THEN RenameVar `n' 2 THEN RenameVar `a' 3) }

1
1. p : ℕ+
2. n : ℕ
3. a : p-adics(p)
⊢ bpa-norm(p;<n, a>) ∈ padic(p)

---

Latex:

---

Latex:
\mforall{}[p:\mBbbN{}\msupplus{}].  \mforall{}[x:basic-padic(p)].    (bpa-norm(p;x)  \mmember{}  padic(p))


By

---

Latex:
((Intros  THEN  Unhide)  THEN  D  2  THEN  RenameVar  `n'  2  THEN  RenameVar  `a'  3)

---

Home Index