---

Step * of Lemma mkpadic_functionality

∀[p:{2...}]. ∀[n,m:ℕ]. ∀[a,b:p-adics(p)].  (a/p^n) = (b/p^m) ∈ padic(p) supposing bpa-equiv(p;<n, a>;<m, b>)
BY
{ (Auto THEN (RWO "bpa-equiv-iff-norm" (-1) THENA Auto) THEN Fold `mkpadic` (-1)) }

1
1. p : {2...}
2. n : ℕ
3. m : ℕ
4. a : p-adics(p)
5. b : p-adics(p)
6. (a/p^n) = (b/p^m) ∈ basic-padic(p)
⊢ (a/p^n) = (b/p^m) ∈ padic(p)

---

Latex:

---

Latex:
\mforall{}[p:\{2...\}].  \mforall{}[n,m:\mBbbN{}].  \mforall{}[a,b:p-adics(p)].    (a/p\^{}n)  =  (b/p\^{}m)  supposing  bpa-equiv(p;<n,  a><m,  b>)


By

---

Latex:
(Auto  THEN  (RWO  "bpa-equiv-iff-norm"  (-1)  THENA  Auto)  THEN  Fold  `mkpadic`  (-1))

---

Home Index