---

Step * of Lemma integer-sqrt

∀x:ℕ. (∃r:ℕ [(((r * r) ≤ x) ∧ x < (r + 1) * (r + 1))])
BY
{ TACTIC:(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:
TACTIC:(InstLemma  `integer-nth-root`  [\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index