---

Step * of Lemma fastpi-property

∀n:ℕ. (|fastpi(n) - π/2(slower)| ≤ (r1/r(10^(20 * 3^n))))
BY
{ InductionOnNat }

1
.....basecase..... 
1. n : ℤ
⊢ |fastpi(0) - π/2(slower)| ≤ (r1/r(10^(20 * 3^0)))

2
.....upcase..... 
1. n : ℤ
2. 0 < n
3. |fastpi(n - 1) - π/2(slower)| ≤ (r1/r(10^(20 * 3^(n - 1))))
⊢ |fastpi(n) - π/2(slower)| ≤ (r1/r(10^(20 * 3^n)))

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  (|fastpi(n)  -  \mpi{}/2(slower)|  \mleq{}  (r1/r(10\^{}(20  *  3\^{}n))))


By

---

Latex:
InductionOnNat

---

Home Index