---

Step * of Lemma p-int-eventually-constant

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

---

Latex:

---

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


By

---

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

---

Home Index