---

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

.....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))
BY
{ xxxD -1xxx }

1
1. x : ℤ
2. [%1] : 0 < x
3. m : {0...}
4. (∀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:
.....upcase..... 
1.  x  :  \mBbbZ{}
2.  [\%1]  :  0  <  x
3.  \mexists{}m:\{0...\}.  ((\mforall{}k:\mBbbN{}m.  x  -  1  <z  k  *  k  =  ff)  \mwedge{}  (\mforall{}k:\{m...\}.  x  -  1  <z  k  *  k  =  tt))
\mvdash{}  \mexists{}m:\{0...\}.  ((\mforall{}k:\mBbbN{}m.  x  <z  k  *  k  =  ff)  \mwedge{}  (\mforall{}k:\{m...\}.  x  <z  k  *  k  =  tt))


By

---

Latex:
xxxD  -1xxx

---

Home Index