---

Step * of Lemma rinv-exp-converges-ext

∀M:ℕ+. ∀N:{2...}.  lim n→∞.(r1/r(M * N^n)) = r0
BY
{ Extract of Obid: rinv-exp-converges
  normalizes to:
  
  λM,N,k. exp-ratio(1;N;0;k;M)
  
  not unfolding  exp-ratio
  finishing with Auto }

---

Latex:

---

Latex:
\mforall{}M:\mBbbN{}\msupplus{}.  \mforall{}N:\{2...\}.    lim  n\mrightarrow{}\minfty{}.(r1/r(M  *  N\^{}n))  =  r0


By

---

Latex:
Extract  of  Obid:  rinv-exp-converges
normalizes  to:

\mlambda{}M,N,k.  exp-ratio(1;N;0;k;M)

not  unfolding    exp-ratio
finishing  with  Auto

---

Home Index