Nuprl Lemma : integer-sqrt

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_plus: + less_than: a < b squash: T less_than': less_than'(a;b) true: True and: P ∧ Q uall: [x:A]. B[x] prop: sq_exists: x:A [B[x]] exp: i^n top: Top eq_int: (i =z j) subtract: m ifthenelse: if then else fi  bfalse: ff nat: ge: i ≥  decidable: Dec(P) or: P ∨ Q uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False implies:  Q not: ¬A
Lemmas referenced :  integer-nth-root less_than_wf and_wf le_wf primrec-unroll primrec1_lemma nat_properties decidable__equal_int satisfiable-full-omega-tt intformnot_wf intformeq_wf itermMultiply_wf itermVar_wf itermConstant_wf int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_mul_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_wf itermAdd_wf int_term_value_add_lemma nat_wf
Rules used in proof :  cut introduction extract_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity dependent_functionElimination thin dependent_set_memberEquality natural_numberEquality sqequalRule independent_pairFormation imageMemberEquality hypothesisEquality baseClosed hypothesis isectElimination lambdaFormation setElimination rename hyp_replacement equalitySymmetry applyEquality lambdaEquality imageElimination because_Cache productElimination isect_memberEquality voidElimination voidEquality unionElimination independent_isectElimination dependent_pairFormation int_eqEquality intEquality computeAll productEquality multiplyEquality addEquality

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_35_27
Last ObjectModification: 2019_06_12-PM-00_24_47

Theory : num_thy_1


Home Index