Step
*
1
1
of Lemma
isqrt_wf
1. x : ℕ
2. v : ∃r:ℕ [(((r * r) ≤ x) ∧ x < (r + 1) * (r + 1))]@i
3. (TERMOF{integer-sqrt-ext:o, 1:l} x) = v ∈ (∃r:ℕ [(((r * r) ≤ x) ∧ x < (r + 1) * (r + 1))])
⊢ v ∈ ℕ
BY
{ TACTIC:Auto }
Latex:
Latex:
1. x : \mBbbN{}
2. v : \mexists{}r:\mBbbN{} [(((r * r) \mleq{} x) \mwedge{} x < (r + 1) * (r + 1))]@i
3. (TERMOF\{integer-sqrt-ext:o, 1:l\} x) = v
\mvdash{} v \mmember{} \mBbbN{}
By
Latex:
TACTIC:Auto
Home
Index