Step * 1 of Lemma isqrt_wf


1. : ℕ
⊢ isqrt(x) ∈ ℕ
BY
(Unfold `isqrt` THEN ((GenConclAtAddr [2]) THENA Auto)) }

1
1. : ℕ
2. : ∃r:ℕ [(((r r) ≤ x) ∧ x < (r 1) (r 1))]
3. (TERMOF{integer-sqrt-ext:o, 1:l} x) v ∈ (∃r:ℕ [(((r r) ≤ x) ∧ x < (r 1) (r 1))])
⊢ v ∈ ℕ


Latex:


Latex:

1.  x  :  \mBbbN{}
\mvdash{}  isqrt(x)  \mmember{}  \mBbbN{}


By


Latex:
(Unfold  `isqrt`  0  THEN  ((GenConclAtAddr  [2])  THENA  Auto))




Home Index