Nuprl Lemma : isqrt_wf

[x:ℕ]. (isqrt(x) ∈ ℕ)


Proof




Definitions occuring in Statement :  isqrt: isqrt(x) nat: uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T isqrt: isqrt(x) subtype_rel: A ⊆B all: x:A. B[x] so_lambda: λ2x.t[x] prop: and: P ∧ Q nat: so_apply: x[s] sq_exists: x:A [B[x]] implies:  Q
Lemmas referenced :  nat_wf integer-sqrt-ext subtype_rel_self sq_exists_wf le_wf less_than_wf equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule sqequalHypSubstitution axiomEquality equalityTransitivity hypothesis equalitySymmetry extract_by_obid applyEquality thin instantiate isectElimination functionEquality lambdaEquality productEquality multiplyEquality setElimination rename hypothesisEquality because_Cache addEquality natural_numberEquality lambdaFormation dependent_functionElimination independent_functionElimination

Latex:
\mforall{}[x:\mBbbN{}].  (isqrt(x)  \mmember{}  \mBbbN{})



Date html generated: 2019_06_20-PM-02_36_45
Last ObjectModification: 2019_06_12-PM-00_25_43

Theory : num_thy_1


Home Index