---

Step * of Lemma bpa-norm-padic

∀[p:ℕ+]. ∀[x:padic(p)].  (bpa-norm(p;x) = x ∈ padic(p))
BY
{ (Intros
   THEN All (Unfold `padic`)
   THEN D -1
   THEN RepUR ``bpa-norm`` 0
   THEN AutoSplit
   THEN D -1
   THEN (InstLemma `p-adic-non-decreasing` [⌜p⌝;⌜x1⌝;⌜n⌝;⌜1⌝]⋅ THENA Auto)
   THEN (Assert 0 ≤ (x1 1) BY
               Auto)
   THEN (OReduce 0 THENA Auto)) }

1
1. p : ℕ+
2. n : {1...}
3. x1 : p-adics(p)
4. ¬((x1 1) = 0 ∈ ℤ)
5. (x1 1) ≤ (x1 n)
6. 0 ≤ (x1 1)
⊢ let k,b = p-unitize(p;x1;n) in <n - k, b> = <n, x1> ∈ (n:ℕ × if (n =z 0) then p-adics(p) else p-units(p) fi )

---

Latex:

---

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


By

---

Latex:
(Intros
  THEN  All  (Unfold  `padic`)
  THEN  D  -1
  THEN  RepUR  ``bpa-norm``  0
  THEN  AutoSplit
  THEN  D  -1
  THEN  (InstLemma  `p-adic-non-decreasing`  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  0  \mleq{}  (x1  1)  BY
                          Auto)
  THEN  (OReduce  0  THENA  Auto))

---

Home Index