---

Step * of Lemma small-real-test_wf

∀[k:ℕ+]. ∀[z:ℝ].  (small-real-test(k;z) ∈ ((r1)/k < z) ∨ (z < (r(4))/k))
BY
{ ProveWfLemma }

1
1. k : ℕ+
2. z : ℝ
⊢ k ∈ (r1)/k < (r(4))/k

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}\msupplus{}].  \mforall{}[z:\mBbbR{}].    (small-real-test(k;z)  \mmember{}  ((r1)/k  <  z)  \mvee{}  (z  <  (r(4))/k))


By

---

Latex:
ProveWfLemma

---

Home Index