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


1. {2...}
2. : ℤ
3. 0 ≤ k
4. : ℕ+
5. k < p^n
6. {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