---

Step * 1 1 1 1 of Lemma fastpi-converges


1. k : ℕ+
2. v : ℕ
3. k ≤ 10^20^3^v
4. cubic_converge(10^20;k) = v ∈ {n:ℕ| k ≤ 10^20^3^n} 
⊢ k ≤ 10^20 * 3^v
BY
{ (Subst'  ⌜10^20 * 3^v = 10^20^3^v ∈ ℤ⌝ 0⋅ THENM Trivial) }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
2.  v  :  \mBbbN{}
3.  k  \mleq{}  10\^{}20\^{}3\^{}v
4.  cubic\_converge(10\^{}20;k)  =  v
\mvdash{}  k  \mleq{}  10\^{}20  *  3\^{}v


By

---

Latex:
(Subst'    \mkleeneopen{}10\^{}20  *  3\^{}v  =  10\^{}20\^{}3\^{}v\mkleeneclose{}  0\mcdot{}  THENM  Trivial)

---

Home Index