Step
*
of Lemma
isqrt-property
∀[x:ℕ]. (((isqrt(x) * isqrt(x)) ≤ x) ∧ x < (isqrt(x) + 1) * (isqrt(x) + 1))
BY
{ xxx(D 0 THENA Auto)xxx }
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:
xxx(D  0  THENA  Auto)xxx
Home
Index