Step
*
1
of Lemma
p-unitize_wf
1. p : ℕ+
2. a : p-adics(p)
3. n : ℕ+
4. ¬((a n) = 0 ∈ ℤ)
5. greatest-p-zero(n;a) = 0 ∈ ℤ
⊢ eval k = greatest-p-zero(n;a) in
<k, if k=0 then a else p-shift(p;a;k)> ∈ k:ℕn + 1 × {b:p-units(p)| p^k(p) * b = a ∈ p-adics(p)}
BY
{ ((HypSubst' (-1) 0 THEN Reduce 0 THEN Auto) THEN MemTypeCD THEN Auto) }
1
1. p : ℕ+
2. a : p-adics(p)
3. n : ℕ+
4. ¬((a n) = 0 ∈ ℤ)
5. greatest-p-zero(n;a) = 0 ∈ ℤ
⊢ a ∈ p-units(p)
2
.....set predicate.....
1. p : ℕ+
2. a : p-adics(p)
3. n : ℕ+
4. ¬((a n) = 0 ∈ ℤ)
5. greatest-p-zero(n;a) = 0 ∈ ℤ
⊢ 1(p) * a = a ∈ p-adics(p)
Latex:
Latex:
1. p : \mBbbN{}\msupplus{}
2. a : p-adics(p)
3. n : \mBbbN{}\msupplus{}
4. \mneg{}((a n) = 0)
5. greatest-p-zero(n;a) = 0
\mvdash{} eval k = greatest-p-zero(n;a) in
<k, if k=0 then a else p-shift(p;a;k)> \mmember{} k:\mBbbN{}n + 1 \mtimes{} \{b:p-units(p)| p\^{}k(p) * b = a\}
By
Latex:
((HypSubst' (-1) 0 THEN Reduce 0 THEN Auto) THEN MemTypeCD THEN Auto)
Home
Index