---

Step * 1 of Lemma rinv-exp-converges


1. M : ℕ+
2. N : {2...}
3. k : ℕ+
4. exp-ratio(1;N;0;k;M) ∈ {n:ℕ| k < M * N^n} 
5. n : ℕ
6. exp-ratio(1;N;0;k;M) ≤ n
⊢ |(r1/r(M * N^n)) - r0| ≤ (r1/r(k))
BY
{ ((Assert r0 < r(M * N^n) BY Auto) THEN (nRNorm 0 THENA Auto)) }

1
1. M : ℕ+
2. N : {2...}
3. k : ℕ+
4. exp-ratio(1;N;0;k;M) ∈ {n:ℕ| k < M * N^n} 
5. n : ℕ
6. exp-ratio(1;N;0;k;M) ≤ n
7. r0 < r(M * N^n)
⊢ |(r1/r(M * N^n))| ≤ (r1/r(k))

---

Latex:

---

Latex:

1.  M  :  \mBbbN{}\msupplus{}
2.  N  :  \{2...\}
3.  k  :  \mBbbN{}\msupplus{}
4.  exp-ratio(1;N;0;k;M)  \mmember{}  \{n:\mBbbN{}|  k  <  M  *  N\^{}n\} 
5.  n  :  \mBbbN{}
6.  exp-ratio(1;N;0;k;M)  \mleq{}  n
\mvdash{}  |(r1/r(M  *  N\^{}n))  -  r0|  \mleq{}  (r1/r(k))


By

---

Latex:
((Assert  r0  <  r(M  *  N\^{}n)  BY  Auto)  THEN  (nRNorm  0  THENA  Auto))

---

Home Index