---

Step * 1 1 1 1 1 1 1 of Lemma rinv-exp-converges


1. M : ℕ+
2. N : {2...}
3. k : ℕ+
4. exp-ratio(1;N;0;k;M) = exp-ratio(1;N;0;k;M) ∈ ℕ
5. k < M * N^exp-ratio(1;N;0;k;M)
6. n : ℕ
7. exp-ratio(1;N;0;k;M) ≤ n
8. r0 < r(M * N^n)
9. m : ℕ
10. (n - exp-ratio(1;N;0;k;M)) = m ∈ ℕ
11. e : ℕ
12. exp-ratio(1;N;0;k;M) = e ∈ ℕ
⊢ N^e ≤ (N^e * N^m)
BY
{ Assert ⌜1 ≤ N^m⌝⋅ }

1
.....assertion..... 
1. M : ℕ+
2. N : {2...}
3. k : ℕ+
4. exp-ratio(1;N;0;k;M) = exp-ratio(1;N;0;k;M) ∈ ℕ
5. k < M * N^exp-ratio(1;N;0;k;M)
6. n : ℕ
7. exp-ratio(1;N;0;k;M) ≤ n
8. r0 < r(M * N^n)
9. m : ℕ
10. (n - exp-ratio(1;N;0;k;M)) = m ∈ ℕ
11. e : ℕ
12. exp-ratio(1;N;0;k;M) = e ∈ ℕ
⊢ 1 ≤ N^m

2
1. M : ℕ+
2. N : {2...}
3. k : ℕ+
4. exp-ratio(1;N;0;k;M) = exp-ratio(1;N;0;k;M) ∈ ℕ
5. k < M * N^exp-ratio(1;N;0;k;M)
6. n : ℕ
7. exp-ratio(1;N;0;k;M) ≤ n
8. r0 < r(M * N^n)
9. m : ℕ
10. (n - exp-ratio(1;N;0;k;M)) = m ∈ ℕ
11. e : ℕ
12. exp-ratio(1;N;0;k;M) = e ∈ ℕ
13. 1 ≤ N^m
⊢ N^e ≤ (N^e * N^m)

---

Latex:

---

Latex:

1.  M  :  \mBbbN{}\msupplus{}
2.  N  :  \{2...\}
3.  k  :  \mBbbN{}\msupplus{}
4.  exp-ratio(1;N;0;k;M)  =  exp-ratio(1;N;0;k;M)
5.  k  <  M  *  N\^{}exp-ratio(1;N;0;k;M)
6.  n  :  \mBbbN{}
7.  exp-ratio(1;N;0;k;M)  \mleq{}  n
8.  r0  <  r(M  *  N\^{}n)
9.  m  :  \mBbbN{}
10.  (n  -  exp-ratio(1;N;0;k;M))  =  m
11.  e  :  \mBbbN{}
12.  exp-ratio(1;N;0;k;M)  =  e
\mvdash{}  N\^{}e  \mleq{}  (N\^{}e  *  N\^{}m)


By

---

Latex:
Assert  \mkleeneopen{}1  \mleq{}  N\^{}m\mkleeneclose{}\mcdot{}

---

Home Index