---

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


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))
BY
{ TACTIC:((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)) }

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

---

Home Index