---

Step * of Lemma p-adic-property

∀p:ℕ+. ∀a:p-adics(p). ∀n:ℕ+. ∀m:{n...}.  ((a m) ≡ (a n) mod p^n)
BY
{ (RepeatFor 3 (Intro)
   THEN (Assert ⌜∀d:ℕ. ((a (n + d)) ≡ (a n) mod p^n)⌝⋅ THENM ((D 0 THENA Auto) THEN D -2 With ⌜m - n⌝  THEN Auto))
   THEN InductionOnNat) }

1
.....basecase..... 
1. p : ℕ+
2. a : p-adics(p)
3. n : ℕ+
⊢ (a (n + 0)) ≡ (a n) mod p^n

2
.....upcase..... 
1. p : ℕ+
2. a : p-adics(p)
3. n : ℕ+
4. d : ℤ
5. [%1] : 0 < d
6. (a (n + (d - 1))) ≡ (a n) mod p^n
⊢ (a (n + d)) ≡ (a n) mod p^n

---

Latex:

---

Latex:
\mforall{}p:\mBbbN{}\msupplus{}.  \mforall{}a:p-adics(p).  \mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}m:\{n...\}.    ((a  m)  \mequiv{}  (a  n)  mod  p\^{}n)


By

---

Latex:
(RepeatFor  3  (Intro)
  THEN  (Assert  \mkleeneopen{}\mforall{}d:\mBbbN{}.  ((a  (n  +  d))  \mequiv{}  (a  n)  mod  p\^{}n)\mkleeneclose{}\mcdot{}
  THENM  ((D  0  THENA  Auto)  THEN  D  -2  With  \mkleeneopen{}m  -  n\mkleeneclose{}    THEN  Auto)
  )
  THEN  InductionOnNat)

---

Home Index