---

Step * 1 1 of Lemma integer-sqrt-xover


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

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

2
.....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))

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}@i
\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:NatInd  1\mcdot{}

---

Home Index