---

Step * 1 1 of Lemma integer-sqrt-xover


1. x : ℕ
⊢ ∃m:{0...}. ((∀k:ℕm. x <z k * k = ff) ∧ (∀k:{m...}. x <z k * k = tt))
BY
{ xxxNatInd 1⋅xxx }

1
.....basecase..... 
∃m:{0...}. ((∀k:ℕm. 0 <z k * k = ff) ∧ (∀k:{m...}. 0 <z k * k = tt))

2
.....upcase..... 
1. x : ℤ
2. [%1] : 0 < x
3. ∃m:{0...}. ((∀k:ℕm. x - 1 <z k * k = ff) ∧ (∀k:{m...}. x - 1 <z k * k = tt))
⊢ ∃m:{0...}. ((∀k:ℕm. x <z k * k = ff) ∧ (∀k:{m...}. x <z k * k = tt))

---

Latex:

---

Latex:

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


By

---

Latex:
xxxNatInd  1\mcdot{}xxx

---

Home Index