---

Step * 1 of Lemma fastpi-converges

.....assertion..... 
1. k : ℕ+
⊢ ∃n:ℕ. (k ≤ 10^20 * 3^n)
BY
{ (D 0 With ⌜eval b = 10^20 in cubic_converge(b;k)⌝  THEN Auto) }

1
1. k : ℕ+
⊢ k ≤ 10^20 * 3^eval b = 10^20 in cubic_converge(b;k)

---

Latex:

---

Latex:
.....assertion..... 
1.  k  :  \mBbbN{}\msupplus{}
\mvdash{}  \mexists{}n:\mBbbN{}.  (k  \mleq{}  10\^{}20  *  3\^{}n)


By

---

Latex:
(D  0  With  \mkleeneopen{}eval  b  =  10\^{}20  in  cubic\_converge(b;k)\mkleeneclose{}    THEN  Auto)

---

Home Index