Nuprl Lemma : integer-sqrt-newton

x:ℕ(∃r:ℕ [(((r r) ≤ x) ∧ x < (r 1) (r 1))])


Proof




Definitions occuring in Statement :  nat: less_than: a < b le: A ≤ B all: x:A. B[x] sq_exists: x:A [B[x]] and: P ∧ Q multiply: m add: m natural_number: $n
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T nat: decidable: Dec(P) or: P ∨ Q uall: [x:A]. B[x] uimplies: supposing a sq_type: SQType(T) implies:  Q guard: {T} and: P ∧ Q cand: c∧ B le: A ≤ B less_than': less_than'(a;b) false: False not: ¬A prop: less_than: a < b squash: T true: True sq_exists: x:A [B[x]] nat_plus: + iff: ⇐⇒ Q rev_implies:  Q uiff: uiff(P;Q) subtype_rel: A ⊆B top: Top subtract: m ge: i ≥  satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x]
Lemmas referenced :  two-mul add-swap one-mul mul-commutes mul-distributes-right mul-distributes int_formula_prop_wf int_formula_prop_le_lemma int_term_value_mul_lemma int_term_value_constant_lemma int_term_value_add_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma intformle_wf itermMultiply_wf itermConstant_wf itermAdd_wf itermVar_wf intformless_wf intformnot_wf intformand_wf satisfiable-full-omega-tt nat_properties square_non_neg minus-zero minus-add add-commutes condition-implies-le le-add-cancel zero-add add-zero add-associates add_functionality_wrt_le not-equal-2 not-lt-2 decidable__lt isqrt_newton_wf less_than_wf and_wf le_wf false_wf nat_wf int_subtype_base subtype_base_sq decidable__equal_int
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin setElimination rename hypothesisEquality natural_numberEquality hypothesis unionElimination instantiate isectElimination cumulativity intEquality independent_isectElimination because_Cache independent_functionElimination introduction sqequalRule independent_pairFormation multiplyEquality equalityTransitivity equalitySymmetry addEquality imageMemberEquality baseClosed dependent_set_memberEquality productElimination voidElimination applyEquality lambdaEquality isect_memberEquality voidEquality minusEquality dependent_pairFormation int_eqEquality computeAll

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



Date html generated: 2019_06_20-PM-02_36_14
Last ObjectModification: 2019_06_12-PM-00_25_16

Theory : num_thy_1


Home Index