---

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


1. p : {2...}
2. k : ℕ+
3. ∃n:ℕ+. k < p^n
⊢ ∃n:ℕ+. ∀m:{n...}. ((-k(p) m) = (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) = (p^m - k) ∈ ℤ

---

Latex:

---

Latex:

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


By

---

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

---

Home Index