Nuprl Lemma : isqrtn_wf

x:ℕ(isqrtn(x) ∈ {r:ℕ((r r) ≤ x) ∧ x < (r 1) (r 1)} )


Proof




Definitions occuring in Statement :  isqrtn: isqrtn(x) nat: less_than: a < b le: A ≤ B all: x:A. B[x] and: P ∧ Q member: t ∈ T set: {x:A| B[x]}  multiply: m add: m natural_number: $n
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T isqrtn: isqrtn(x) subtype_rel: A ⊆B uall: [x:A]. B[x] so_lambda: λ2x.t[x] prop: and: P ∧ Q nat: so_apply: x[s] sq_exists: x:A [B[x]]
Lemmas referenced :  integer-sqrt-newton-ext subtype_rel_self nat_wf sq_exists_wf le_wf less_than_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequalRule applyEquality thin instantiate extract_by_obid hypothesis introduction sqequalHypSubstitution isectElimination functionEquality lambdaEquality productEquality multiplyEquality setElimination rename hypothesisEquality because_Cache addEquality natural_numberEquality setEquality

Latex:
\mforall{}x:\mBbbN{}.  (isqrtn(x)  \mmember{}  \{r:\mBbbN{}|  ((r  *  r)  \mleq{}  x)  \mwedge{}  x  <  (r  +  1)  *  (r  +  1)\}  )



Date html generated: 2018_05_21-PM-07_52_09
Last ObjectModification: 2018_05_19-PM-04_49_45

Theory : general


Home Index