Step
*
1
2
1
1
of Lemma
integer-sqrt-bin-search
1. x : ℕ@i
2. ¬x < 2
⊢ ↓∃x1:ℕx. ((∀y:ℕx1 + 1. (¬↑x <z y * y)) ∧ (∀z:{x1 + 1..x + 1-}. (↑x <z z * z)))
BY
{ Assert ⌜∃z:ℤ. (((z * z) ≤ x) ∧ x < (z + 1) * (z + 1))⌝⋅ }
1
.....assertion.....
1. x : ℕ@i
2. ¬x < 2
⊢ ∃z:ℤ. (((z * z) ≤ x) ∧ x < (z + 1) * (z + 1))
2
1. x : ℕ@i
2. ¬x < 2
3. ∃z:ℤ. (((z * z) ≤ x) ∧ x < (z + 1) * (z + 1))
⊢ ↓∃x1:ℕx. ((∀y:ℕx1 + 1. (¬↑x <z y * y)) ∧ (∀z:{x1 + 1..x + 1-}. (↑x <z z * z)))
Latex:
Latex:
1. x : \mBbbN{}@i
2. \mneg{}x < 2
\mvdash{} \mdownarrow{}\mexists{}x1:\mBbbN{}x. ((\mforall{}y:\mBbbN{}x1 + 1. (\mneg{}\muparrow{}x <z y * y)) \mwedge{} (\mforall{}z:\{x1 + 1..x + 1\msupminus{}\}. (\muparrow{}x <z z * z)))
By
Latex:
Assert \mkleeneopen{}\mexists{}z:\mBbbZ{}. (((z * z) \mleq{} x) \mwedge{} x < (z + 1) * (z + 1))\mkleeneclose{}\mcdot{}
Home
Index