---

Step * 2 of Lemma p-int-eventually-constant


1. p : {2...}
2. k : ℕ
3. ∃n:ℕ+. k < p^n
⊢ ∃n:ℕ+. ∀m:{n...}. ((k(p) m) = k ∈ ℤ)
BY
{ ((ParallelLast THEN Auto) THEN RepUR ``p-int p-reduce`` 0) }

1
1. p : {2...}
2. k : ℕ
3. n : ℕ+
4. k < p^n
5. m : {n...}
⊢ (k mod p^m) = k ∈ ℤ

---

Latex:

---

Latex:

1.  p  :  \{2...\}
2.  k  :  \mBbbN{}
3.  \mexists{}n:\mBbbN{}\msupplus{}.  k  <  p\^{}n
\mvdash{}  \mexists{}n:\mBbbN{}\msupplus{}.  \mforall{}m:\{n...\}.  ((k(p)  m)  =  k)


By

---

Latex:
((ParallelLast  THEN  Auto)  THEN  RepUR  ``p-int  p-reduce``  0)

---

Home Index