---

Step * 1 1 1 of Lemma mkpadic_functionality


1. p : {2...}
2. v : padic(p)
3. v1 : padic(p)
4. v = v1 ∈ (ℕ × p-adics(p))
⊢ v = v1 ∈ padic(p)
BY
{ ((D -3 THEN D -2) THEN (EqHD (-1) THENA Auto) THEN All Reduce) }

1
1. p : {2...}
2. n : ℕ
3. v2 : if (n =z 0) then p-adics(p) else p-units(p) fi 
4. n1 : ℕ
5. v3 : if (n1 =z 0) then p-adics(p) else p-units(p) fi 
6. n = n1 ∈ ℕ
7. v2 = v3 ∈ p-adics(p)
⊢ <n, v2> = <n1, v3> ∈ padic(p)

---

Latex:

---

Latex:

1.  p  :  \{2...\}
2.  v  :  padic(p)
3.  v1  :  padic(p)
4.  v  =  v1
\mvdash{}  v  =  v1


By

---

Latex:
((D  -3  THEN  D  -2)  THEN  (EqHD  (-1)  THENA  Auto)  THEN  All  Reduce)

---

Home Index