---

Step * of Lemma integer-sqrt

∀x:ℕ. (∃r:{ℕ| (((r * r) ≤ x) ∧ x < (r + 1) * (r + 1))})
BY
{ (InstLemma `integer-nth-root` [⌜2⌝]⋅ THENA Auto) }

1
1. ∀x:ℕ. (∃r:{ℕ| ((r^2 ≤ x) ∧ x < r + 1^2)})
⊢ ∀x:ℕ. (∃r:{ℕ| (((r * r) ≤ x) ∧ x < (r + 1) * (r + 1))})

---

Latex:

---

Latex:
\mforall{}x:\mBbbN{}.  (\mexists{}r:\{\mBbbN{}|  (((r  *  r)  \mleq{}  x)  \mwedge{}  x  <  (r  +  1)  *  (r  +  1))\})


By

---

Latex:
(InstLemma  `integer-nth-root`  [\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index