---

Step * of Lemma isqrt_newton_wf

∀n,x:ℕ+.  isqrt_newton(n;x) ∈ ∃r:ℕ [(((r * r) ≤ n) ∧ n < (r + 1) * (r + 1))] supposing n < (x + 1) * (x + 1)
BY
{ (Assert ⌜∀d:ℕ. ∀n,x:ℕ+.
             (((((x + 1) * (x + 1)) - n) ≤ d)
             ⇒ n < (x + 1) * (x + 1)
             ⇒ (isqrt_newton(n;x) ∈ ∃r:ℕ [(((r * r) ≤ n) ∧ n < (r + 1) * (r + 1))]))⌝⋅
THENM (Auto THEN InstHyp [⌜((x + 1) * (x + 1)) - n⌝;⌜n⌝;⌜x⌝] 1⋅ THEN Auto)
) }

1
.....assertion..... 
∀d:ℕ. ∀n,x:ℕ+.
  (((((x + 1) * (x + 1)) - n) ≤ d)
  ⇒ n < (x + 1) * (x + 1)
  ⇒ (isqrt_newton(n;x) ∈ ∃r:ℕ [(((r * r) ≤ n) ∧ n < (r + 1) * (r + 1))]))

---

Latex:

---

Latex:
\mforall{}n,x:\mBbbN{}\msupplus{}.
    isqrt\_newton(n;x)  \mmember{}  \mexists{}r:\mBbbN{}  [(((r  *  r)  \mleq{}  n)  \mwedge{}  n  <  (r  +  1)  *  (r  +  1))]  supposing  n  <  (x  +  1)  *  (x  +  1)


By

---

Latex:
(Assert  \mkleeneopen{}\mforall{}d:\mBbbN{}.  \mforall{}n,x:\mBbbN{}\msupplus{}.
                      (((((x  +  1)  *  (x  +  1))  -  n)  \mleq{}  d)
                      {}\mRightarrow{}  n  <  (x  +  1)  *  (x  +  1)
                      {}\mRightarrow{}  (isqrt\_newton(n;x)  \mmember{}  \mexists{}r:\mBbbN{}  [(((r  *  r)  \mleq{}  n)  \mwedge{}  n  <  (r  +  1)  *  (r  +  1))]))\mkleeneclose{}\mcdot{}
THENM  (Auto  THEN  InstHyp  [\mkleeneopen{}((x  +  1)  *  (x  +  1))  -  n\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  1\mcdot{}  THEN  Auto)
)

---

Home Index