---

Step * of Lemma p-minus-int-eventually

∀p:{2...}. ∀k:ℕ+.  ∃n:ℕ+. ∀m:{n...}. ((-k(p) m) = (p^m - k) ∈ ℤ)
BY
{ (Auto THEN Assert ⌜∃n:ℕ+. k < p^n⌝⋅) }

1
.....assertion..... 
1. p : {2...}
2. k : ℕ+
⊢ ∃n:ℕ+. k < p^n

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

---

Latex:

---

Latex:
\mforall{}p:\{2...\}.  \mforall{}k:\mBbbN{}\msupplus{}.    \mexists{}n:\mBbbN{}\msupplus{}.  \mforall{}m:\{n...\}.  ((-k(p)  m)  =  (p\^{}m  -  k))


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}\mexists{}n:\mBbbN{}\msupplus{}.  k  <  p\^{}n\mkleeneclose{}\mcdot{})

---

Home Index