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