Step
*
2
1
of Lemma
exp-ratio_wf2
1. b : {2...}
2. k : ℕ
3. M : ℕ+
4. ∀c:{n:ℕ| k < M * b^n} . ∀n:ℕ. ((n ≤ c)
⇒ (exp-ratio(1;b;n;k;M * b^n) ∈ {n:ℕ| k < M * b^n} ))
⊢ exp-ratio(1;b;0;k;M) ∈ {n:ℕ| k < M * b^n}
BY
{ Assert ⌜∃c:ℕ. k < M * b^c⌝⋅ }
1
.....assertion.....
1. b : {2...}
2. k : ℕ
3. M : ℕ+
4. ∀c:{n:ℕ| k < M * b^n} . ∀n:ℕ. ((n ≤ c)
⇒ (exp-ratio(1;b;n;k;M * b^n) ∈ {n:ℕ| k < M * b^n} ))
⊢ ∃c:ℕ. k < M * b^c
2
1. b : {2...}
2. k : ℕ
3. M : ℕ+
4. ∀c:{n:ℕ| k < M * b^n} . ∀n:ℕ. ((n ≤ c)
⇒ (exp-ratio(1;b;n;k;M * b^n) ∈ {n:ℕ| k < M * b^n} ))
5. ∃c:ℕ. k < M * b^c
⊢ exp-ratio(1;b;0;k;M) ∈ {n:ℕ| k < M * b^n}
Latex:
Latex:
1. b : \{2...\}
2. k : \mBbbN{}
3. M : \mBbbN{}\msupplus{}
4. \mforall{}c:\{n:\mBbbN{}| k < M * b\^{}n\} . \mforall{}n:\mBbbN{}. ((n \mleq{} c) {}\mRightarrow{} (exp-ratio(1;b;n;k;M * b\^{}n) \mmember{} \{n:\mBbbN{}| k < M * b\^{}n\} ))
\mvdash{} exp-ratio(1;b;0;k;M) \mmember{} \{n:\mBbbN{}| k < M * b\^{}n\}
By
Latex:
Assert \mkleeneopen{}\mexists{}c:\mBbbN{}. k < M * b\^{}c\mkleeneclose{}\mcdot{}
Home
Index