---

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
{ TACTIC:(With ⌜1⌝ (D 0)⋅ THEN Reduce 0 THEN Auto) }

1
1. k : ℕ1@i
⊢ 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:
TACTIC:(With  \mkleeneopen{}1\mkleeneclose{}  (D  0)\mcdot{}  THEN  Reduce  0  THEN  Auto)

---

Home Index