Nuprl Lemma : isqrt-property

[x:ℕ]. (((isqrt(x) isqrt(x)) ≤ x) ∧ x < (isqrt(x) 1) (isqrt(x) 1))


Proof




Definitions occuring in Statement :  isqrt: isqrt(x) nat: less_than: a < b uall: [x:A]. B[x] le: A ≤ B and: P ∧ Q multiply: m add: m natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T and: P ∧ Q le: A ≤ B not: ¬A implies:  Q false: False nat: subtype_rel: A ⊆B prop: uimplies: supposing a isqrt: isqrt(x) all: x:A. B[x] so_lambda: λ2x.t[x] so_apply: x[s] sq_exists: x:A [B[x]] cand: c∧ B ge: i ≥  decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top sq_stable: SqStable(P) squash: T
Lemmas referenced :  less_than'_wf isqrt_wf nat_wf member-less_than integer-sqrt-ext subtype_rel_self sq_exists_wf le_wf less_than_wf nat_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermMultiply_wf itermVar_wf intformless_wf itermAdd_wf itermConstant_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_mul_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_term_value_add_lemma int_term_value_constant_lemma sq_stable__le int_formula_prop_wf equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule sqequalHypSubstitution productElimination thin independent_pairEquality lambdaEquality dependent_functionElimination hypothesisEquality voidElimination extract_by_obid isectElimination setElimination rename hypothesis multiplyEquality applyEquality because_Cache axiomEquality equalityTransitivity equalitySymmetry addEquality natural_numberEquality independent_isectElimination instantiate functionEquality productEquality lambdaFormation unionElimination approximateComputation independent_functionElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidEquality independent_pairFormation imageMemberEquality baseClosed imageElimination

Latex:
\mforall{}[x:\mBbbN{}].  (((isqrt(x)  *  isqrt(x))  \mleq{}  x)  \mwedge{}  x  <  (isqrt(x)  +  1)  *  (isqrt(x)  +  1))



Date html generated: 2019_06_20-PM-02_36_53
Last ObjectModification: 2019_06_12-PM-00_25_48

Theory : num_thy_1


Home Index