---

Step * 3 of Lemma isqrrrt


∀n:ℕ+. ((∃r:ℕ [(((r * r) ≤ (n ÷ 4)) ∧ n ÷ 4 < (r + 1) * (r + 1))]) ⇒ (∃r:ℕ [(((r * r) ≤ n) ∧ n < (r + 1) * (r + 1))]))
BY
{ RepeatFor 2 ((D 0 THENA Auto)) }

1
1. n : ℕ+
2. ∃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{}\msupplus{}
    ((\mexists{}r:\mBbbN{}  [(((r  *  r)  \mleq{}  (n  \mdiv{}  4))  \mwedge{}  n  \mdiv{}  4  <  (r  +  1)  *  (r  +  1))])
    {}\mRightarrow{}  (\mexists{}r:\mBbbN{}  [(((r  *  r)  \mleq{}  n)  \mwedge{}  n  <  (r  +  1)  *  (r  +  1))]))


By

---

Latex:
RepeatFor  2  ((D  0  THENA  Auto))

---

Home Index