---

Step * of Lemma fastpi-converges

lim n→∞.fastpi(n) = π/2(slower)
BY
{ ((D 0 THENA Auto) THEN Assert ⌜∃n:ℕ. (k ≤ 10^20 * 3^n)⌝⋅) }

1
.....assertion..... 
1. k : ℕ+
⊢ ∃n:ℕ. (k ≤ 10^20 * 3^n)

2
1. k : ℕ+
2. ∃n:ℕ. (k ≤ 10^20 * 3^n)
⊢ ∃N:{ℕ| (∀n:ℕ. ((N ≤ n) ⇒ (|fastpi(n) - π/2(slower)| ≤ (r1/r(k)))))}

---

Latex:

---

Latex:
lim  n\mrightarrow{}\minfty{}.fastpi(n)  =  \mpi{}/2(slower)


By

---

Latex:
((D  0  THENA  Auto)  THEN  Assert  \mkleeneopen{}\mexists{}n:\mBbbN{}.  (k  \mleq{}  10\^{}20  *  3\^{}n)\mkleeneclose{}\mcdot{})

---

Home Index