---

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


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))
BY
{ xxx((RWO "eqtt_to_assert eqff_to_assert" (-1) THENA Auto)
      THEN (RW assert_pushdownC (-1) THENA Auto)
      THEN (RWO "eqtt_to_assert eqff_to_assert" 0 THENA Auto)
      THEN (RW assert_pushdownC 0 THENA Auto))xxx }

1
1. x : ℤ
2. [%1] : 0 < x
3. m : {0...}
4. (∀k:ℕm. (¬x - 1 < k * k)) ∧ (∀k:{m...}. x - 1 < k * k)
⊢ ∃m:{0...}. ((∀k:ℕm. (¬x < k * k)) ∧ (∀k:{m...}. x < k * k))

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}
2.  [\%1]  :  0  <  x
3.  m  :  \{0...\}
4.  (\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:
xxx((RWO  "eqtt\_to\_assert  eqff\_to\_assert"  (-1)  THENA  Auto)
        THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto)
        THEN  (RWO  "eqtt\_to\_assert  eqff\_to\_assert"  0  THENA  Auto)
        THEN  (RW  assert\_pushdownC  0  THENA  Auto))xxx

---

Home Index