---

Step * 1 1 1 of Lemma integer-sqrt-xover

.....basecase..... 
∃m:{0...}. ((∀k:ℕm. 0 <z k * k = ff) ∧ (∀k:{m...}. 0 <z k * k = tt))
BY
{ xxx(With ⌜1⌝ (D 0)⋅ THEN Reduce 0 THEN Auto)xxx }

1
1. k : ℕ1
⊢ 0 <z k * k = ff

---

Latex:

---

Latex:
.....basecase..... 
\mexists{}m:\{0...\}.  ((\mforall{}k:\mBbbN{}m.  0  <z  k  *  k  =  ff)  \mwedge{}  (\mforall{}k:\{m...\}.  0  <z  k  *  k  =  tt))


By

---

Latex:
xxx(With  \mkleeneopen{}1\mkleeneclose{}  (D  0)\mcdot{}  THEN  Reduce  0  THEN  Auto)xxx

---

Home Index