---

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


1. p : {2...}
2. k : ℕ
3. ¬(k = 0 ∈ ℤ)
⊢ ∃n:ℕ+. k < p^n
BY
{ (D 0 With ⌜log(p;k) + 1⌝ 
   THEN Auto
   THEN InstLemma `log-property` [⌜p⌝;⌜k⌝]⋅
   THEN Auto
   THEN (RWO "exp_add" 0 THENA Auto)
   THEN (RWO "exp1" 0 THENA Auto)
   THEN RWO "-1<" 0
   THEN Auto) }

1
1. p : {2...}
2. k : ℕ
3. ¬(k = 0 ∈ ℤ)
4. k ≤ p^log(p;k)
⊢ k < k * p

---

Latex:

---

Latex:

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


By

---

Latex:
(D  0  With  \mkleeneopen{}log(p;k)  +  1\mkleeneclose{} 
  THEN  Auto
  THEN  InstLemma  `log-property`  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  (RWO  "exp\_add"  0  THENA  Auto)
  THEN  (RWO  "exp1"  0  THENA  Auto)
  THEN  RWO  "-1<"  0
  THEN  Auto)

---

Home Index