---

Step * of Lemma p-unitize-unit

∀p:ℕ+. ∀a:p-units(p). ∀n:ℕ+.  (p-unitize(p;a;n) = <0, a> ∈ (k:ℕ × {b:p-units(p)| p^k(p) * b = a ∈ p-adics(p)} ))
BY
{ (Auto
   THEN D 2
   THEN Unfold `p-unitize` 0
   THEN (Subst' greatest-p-zero(n;a) ~ 0 0
   THENM (Reduce 0 THEN Fold `member` 0 THEN (MemCD THEN Auto) THEN MemTypeCD THEN Auto)
   )) }

1
.....equality..... 
1. p : ℕ+
2. a : p-adics(p)
3. ¬((a 1) = 0 ∈ ℤ)
4. n : ℕ+
⊢ greatest-p-zero(n;a) ~ 0

2
.....set predicate..... 
1. p : ℕ+
2. a : p-adics(p)
3. ¬((a 1) = 0 ∈ ℤ)
4. n : ℕ+
⊢ 1(p) * a = a ∈ p-adics(p)

---

Latex:

---

Latex:
\mforall{}p:\mBbbN{}\msupplus{}.  \mforall{}a:p-units(p).  \mforall{}n:\mBbbN{}\msupplus{}.    (p-unitize(p;a;n)  =  ɘ,  a>)


By

---

Latex:
(Auto
  THEN  D  2
  THEN  Unfold  `p-unitize`  0
  THEN  (Subst'  greatest-p-zero(n;a)  \msim{}  0  0
  THENM  (Reduce  0  THEN  Fold  `member`  0  THEN  (MemCD  THEN  Auto)  THEN  MemTypeCD  THEN  Auto)
  ))

---

Home Index