---

Step * 1 2 1 1 1 1 of Lemma integer-sqrt-bin-search


1. x : ℕ@i
2. ¬x < 2
⊢ ((iroot(2;x) * iroot(2;x)) ≤ x) ∧ x < (iroot(2;x) + 1) * (iroot(2;x) + 1)
BY
{ (InstLemma `iroot-property` [⌜2⌝;⌜x⌝]⋅ THENA Auto) }

1
1. x : ℕ@i
2. ¬x < 2
3. (iroot(2;x)^2 ≤ x) ∧ x < iroot(2;x) + 1^2
⊢ ((iroot(2;x) * iroot(2;x)) ≤ x) ∧ x < (iroot(2;x) + 1) * (iroot(2;x) + 1)

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}@i
2.  \mneg{}x  <  2
\mvdash{}  ((iroot(2;x)  *  iroot(2;x))  \mleq{}  x)  \mwedge{}  x  <  (iroot(2;x)  +  1)  *  (iroot(2;x)  +  1)


By

---

Latex:
(InstLemma  `iroot-property`  [\mkleeneopen{}2\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index