---

Step * 1 of Lemma mkpadic_functionality


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)
BY
{ (MoveToConcl (-1) THEN GenConclTerms Auto [⌜(a/p^n)⌝;⌜(b/p^m)⌝]⋅ THEN All Thin) }

1
1. p : {2...}
2. v : padic(p)
3. v1 : padic(p)
⊢ (v = v1 ∈ basic-padic(p)) ⇒ (v = v1 ∈ padic(p))

---

Latex:

---

Latex:

1.  p  :  \{2...\}
2.  n  :  \mBbbN{}
3.  m  :  \mBbbN{}
4.  a  :  p-adics(p)
5.  b  :  p-adics(p)
6.  (a/p\^{}n)  =  (b/p\^{}m)
\mvdash{}  (a/p\^{}n)  =  (b/p\^{}m)


By

---

Latex:
(MoveToConcl  (-1)  THEN  GenConclTerms  Auto  [\mkleeneopen{}(a/p\^{}n)\mkleeneclose{};\mkleeneopen{}(b/p\^{}m)\mkleeneclose{}]\mcdot{}  THEN  All  Thin)

---

Home Index