---

Step * of Lemma p-digit_wf

No Annotations
∀[p:ℕ+]. ∀[a:p-adics(p)]. ∀[n:ℕ+].  (p-digit(p;a;n) ∈ ℕp)
BY
{ (Auto THEN D 2 THEN CaseNat 1 `n') }

1
1. p : ℕ+
2. a : n:ℕ+ ⟶ ℕp^n
3. ∀n:ℕ+. ((a (n + 1)) ≡ (a n) mod p^n)
4. n : ℕ+
5. n = 1 ∈ ℤ
⊢ p-digit(p;a;1) ∈ ℕp

2
1. p : ℕ+
2. a : n:ℕ+ ⟶ ℕp^n
3. ∀n:ℕ+. ((a (n + 1)) ≡ (a n) mod p^n)
4. n : ℕ+
5. ¬(n = 1 ∈ ℤ)
⊢ p-digit(p;a;n) ∈ ℕp

---

Latex:

---

Latex:
No  Annotations
\mforall{}[p:\mBbbN{}\msupplus{}].  \mforall{}[a:p-adics(p)].  \mforall{}[n:\mBbbN{}\msupplus{}].    (p-digit(p;a;n)  \mmember{}  \mBbbN{}p)


By

---

Latex:
(Auto  THEN  D  2  THEN  CaseNat  1  `n')

---

Home Index