---

Step * 2 of Lemma fastpi-converges


1. k : ℕ+
2. ∃n:ℕ. (k ≤ 10^20 * 3^n)
⊢ ∃N:{ℕ| (∀n:ℕ. ((N ≤ n) ⇒ (|fastpi(n) - π/2(slower)| ≤ (r1/r(k)))))}
BY
{ ((ExRepD THEN D 0 With ⌜n⌝  THEN Auto) THEN RenameVar `m' (-2) THEN RWO "fastpi-property" 0 THEN Auto) }

1
1. k : ℕ+
2. n : ℕ
3. k ≤ 10^20 * 3^n
4. m : ℕ
5. n ≤ m
⊢ (r1/r(10^20 * 3^m)) ≤ (r1/r(k))

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
2.  \mexists{}n:\mBbbN{}.  (k  \mleq{}  10\^{}20  *  3\^{}n)
\mvdash{}  \mexists{}N:\{\mBbbN{}|  (\mforall{}n:\mBbbN{}.  ((N  \mleq{}  n)  {}\mRightarrow{}  (|fastpi(n)  -  \mpi{}/2(slower)|  \mleq{}  (r1/r(k)))))\}


By

---

Latex:
((ExRepD  THEN  D  0  With  \mkleeneopen{}n\mkleeneclose{}    THEN  Auto)
  THEN  RenameVar  `m'  (-2)
  THEN  RWO  "fastpi-property"  0
  THEN  Auto)

---

Home Index