Step
*
2
1
1
of Lemma
p-int-eventually-constant
1. p : {2...}
2. k : ℤ
3. 0 ≤ k
4. n : ℕ+
5. k < p^n
6. m : {n...}
⊢ k < p^m
BY
{ ((Assert p^n ≤ p^m BY EAuto 1) THEN Auto) }
Latex:
Latex:
1.  p  :  \{2...\}
2.  k  :  \mBbbZ{}
3.  0  \mleq{}  k
4.  n  :  \mBbbN{}\msupplus{}
5.  k  <  p\^{}n
6.  m  :  \{n...\}
\mvdash{}  k  <  p\^{}m
By
Latex:
((Assert  p\^{}n  \mleq{}  p\^{}m  BY  EAuto  1)  THEN  Auto)
Home
Index