---

Step * 1 of Lemma isqrrrt


λn.(∃r:ℕ [(((r * r) ≤ n) ∧ n < (r + 1) * (r + 1))]) ∈ ℕ ⟶ ℙ
BY
{ Auto }

---

Latex:

---

Latex:

\mlambda{}n.(\mexists{}r:\mBbbN{}  [(((r  *  r)  \mleq{}  n)  \mwedge{}  n  <  (r  +  1)  *  (r  +  1))])  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}


By

---

Latex:
Auto

---

Home Index