---

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


1. p : {2...}
2. k : ℕ
3. ¬(k = 0 ∈ ℤ)
4. k ≤ p^log(p;k)
⊢ k < k * p
BY
{ ((Assert 1 < p BY Auto) THEN Mul ⌜k⌝ (-1)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  p  :  \{2...\}
2.  k  :  \mBbbN{}
3.  \mneg{}(k  =  0)
4.  k  \mleq{}  p\^{}log(p;k)
\mvdash{}  k  <  k  *  p


By

---

Latex:
((Assert  1  <  p  BY  Auto)  THEN  Mul  \mkleeneopen{}k\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto)

---

Home Index