---

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

.....upcase..... 
1. x : ℤ@i
2. [%1] : 0 < x@i
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
{ TACTIC:D -1 }

1
1. x : ℤ@i
2. [%1] : 0 < x@i
3. m : {0...}@i
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{}@i
2.  [\%1]  :  0  <  x@i
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:
TACTIC:D  -1

---

Home Index