---

Step * 1 of Lemma bpa-equiv-iff-norm


1. p : {2...}
2. EquivRel(basic-padic(p);x,y.bpa-equiv(p;x;y))
3. ∀x:basic-padic(p). bpa-equiv(p;x;bpa-norm(p;x))
4. x : basic-padic(p)
5. y : basic-padic(p)
6. bpa-equiv(p;x;y)
⊢ bpa-norm(p;x) = bpa-norm(p;y) ∈ basic-padic(p)
BY
{ ((D -3 THEN RenameVar `n' (-4) THEN RenameVar `a' (-3))
   THEN D -2
   THEN RenameVar `m' (-3)
   THEN RenameVar `b' (-2)
   THEN RepUR ``bpa-equiv`` -1
   THEN RepUR ``bpa-norm`` 0
   THEN AutoSplit) }

1
1. p : {2...}
2. EquivRel(basic-padic(p);x,y.bpa-equiv(p;x;y))
3. ∀x:basic-padic(p). bpa-equiv(p;x;bpa-norm(p;x))
4. n : ℕ
5. a : p-adics(p)
6. m : ℕ
7. b : p-adics(p)
8. p^m(p) * a = p^n(p) * b ∈ p-adics(p)
9. n = 0 ∈ ℤ
⊢ <0, a>
= if (m =z 0) then <0, b>
  if (b m =z 0) then <0, p-shift(p;b;m)>
  else let k,b = p-unitize(p;b;m) 
       in <m - k, b>
  fi 
∈ basic-padic(p)

2
1. p : {2...}
2. EquivRel(basic-padic(p);x,y.bpa-equiv(p;x;y))
3. ∀x:basic-padic(p). bpa-equiv(p;x;bpa-norm(p;x))
4. n : {1...}
5. a : p-adics(p)
6. m : ℕ
7. b : p-adics(p)
8. p^m(p) * a = p^n(p) * b ∈ p-adics(p)
⊢ if (a n =z 0) then <0, p-shift(p;a;n)> else let k,b = p-unitize(p;a;n) in <n - k, b> fi 
= if (m =z 0) then <0, b>
  if (b m =z 0) then <0, p-shift(p;b;m)>
  else let k,b = p-unitize(p;b;m) 
       in <m - k, b>
  fi 
∈ basic-padic(p)

---

Latex:

---

Latex:

1.  p  :  \{2...\}
2.  EquivRel(basic-padic(p);x,y.bpa-equiv(p;x;y))
3.  \mforall{}x:basic-padic(p).  bpa-equiv(p;x;bpa-norm(p;x))
4.  x  :  basic-padic(p)
5.  y  :  basic-padic(p)
6.  bpa-equiv(p;x;y)
\mvdash{}  bpa-norm(p;x)  =  bpa-norm(p;y)


By

---

Latex:
((D  -3  THEN  RenameVar  `n'  (-4)  THEN  RenameVar  `a'  (-3))
  THEN  D  -2
  THEN  RenameVar  `m'  (-3)
  THEN  RenameVar  `b'  (-2)
  THEN  RepUR  ``bpa-equiv``  -1
  THEN  RepUR  ``bpa-norm``  0
  THEN  AutoSplit)

---

Home Index