---

Step * of Lemma isqrt-property

∀[x:ℕ]. (((isqrt(x) * isqrt(x)) ≤ x) ∧ x < (isqrt(x) + 1) * (isqrt(x) + 1))
BY
{ TACTIC:(D 0 THENA Auto) }

1
1. x : ℕ
⊢ ((isqrt(x) * isqrt(x)) ≤ x) ∧ x < (isqrt(x) + 1) * (isqrt(x) + 1)

---

Latex:

---

Latex:
\mforall{}[x:\mBbbN{}].  (((isqrt(x)  *  isqrt(x))  \mleq{}  x)  \mwedge{}  x  <  (isqrt(x)  +  1)  *  (isqrt(x)  +  1))


By

---

Latex:
TACTIC:(D  0  THENA  Auto)

---

Home Index