---

Step * of Lemma isqrrrt

∀n:ℕ. (∃r:ℕ [(((r * r) ≤ n) ∧ n < (r + 1) * (r + 1))])
BY
{ DivNatInduction ⌜4⌝⋅ }

1
λn.(∃r:ℕ [(((r * r) ≤ n) ∧ n < (r + 1) * (r + 1))]) ∈ ℕ ⟶ ℙ

2
∃r:ℕ [(((r * r) ≤ 0) ∧ 0 < (r + 1) * (r + 1))]

3
∀n:ℕ+. ((∃r:ℕ [(((r * r) ≤ (n ÷ 4)) ∧ n ÷ 4 < (r + 1) * (r + 1))]) ⇒ (∃r:ℕ [(((r * r) ≤ n) ∧ n < (r + 1) * (r + 1))]))

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  (\mexists{}r:\mBbbN{}  [(((r  *  r)  \mleq{}  n)  \mwedge{}  n  <  (r  +  1)  *  (r  +  1))])


By

---

Latex:
DivNatInduction  \mkleeneopen{}4\mkleeneclose{}\mcdot{}

---

Home Index