---

Step * of Lemma fastpi_wf

∀n:ℕ. (fastpi(n) ∈ ℝ)
BY
{ InductionOnNat }

1
.....basecase..... 
1. n : ℤ
⊢ fastpi(0) ∈ ℝ

2
.....upcase..... 
1. n : ℤ
2. 0 < n
3. fastpi(n - 1) ∈ ℝ
⊢ fastpi(n) ∈ ℝ

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  (fastpi(n)  \mmember{}  \mBbbR{})


By

---

Latex:
InductionOnNat

---

Home Index