Nuprl Lemma : isqrrrt

n:ℕ(∃r:ℕ [(((r r) ≤ n) ∧ n < (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 :  rev_uimplies: rev_uimplies(P;Q) top: Top exists: x:A. B[x] satisfiable_int_formula: satisfiable_int_formula(fmla) or: P ∨ Q decidable: Dec(P) ge: i ≥  subtype_rel: A ⊆B sq_stable: SqStable(P) sq_type: SQType(T) uimplies: supposing a nequal: a ≠ b ∈  int_nzero: -o nat_plus: + cand: c∧ B not: ¬A false: False le: A ≤ B sq_exists: x:A [B[x]] nat: prop: implies:  Q so_apply: x[s] so_lambda: λ2x.t[x] guard: {T} uall: [x:A]. B[x] and: P ∧ Q true: True less_than': less_than'(a;b) squash: T less_than: a < b member: t ∈ T all: x:A. B[x]
Lemmas referenced :  le_weakening add_functionality_wrt_le less_than_functionality add-commutes add-swap mul-swap mul-commutes add-associates mul-associates mul-distributes-right mul-distributes remainder_wfa mul_preserves_le int_term_value_subtract_lemma itermSubtract_wf subtract_wf int_term_value_mul_lemma int_term_value_add_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_formula_prop_le_lemma int_formula_prop_and_lemma itermMultiply_wf itermAdd_wf intformeq_wf itermVar_wf intformle_wf intformand_wf decidable__le int-value-type equal_wf set-value-type int_formula_prop_wf int_term_value_constant_lemma int_formula_prop_less_lemma istype-void int_formula_prop_not_lemma itermConstant_wf intformless_wf intformnot_wf full-omega-unsat decidable__lt nat_plus_properties nat_properties nat_plus_subtype_nat rem_bounds_1 div_rem_sum member-less_than sq_stable__less_than sq_stable__le sq_stable__and nat_plus_wf nequal_wf istype-int int_subtype_base subtype_base_sq divide_wfa istype-le istype-nat false_wf less_than_wf le_wf nat_wf sq_exists_wf istype-less_than div_nat_induction-ext
Rules used in proof :  int_eqEquality Error :dependent_set_memberFormation_alt,  cutEval Error :dependent_pairFormation_alt,  approximateComputation unionElimination applyEquality imageElimination Error :functionIsTypeImplies,  Error :lambdaEquality_alt,  Error :inhabitedIsType,  closedConclusion Error :isect_memberEquality_alt,  productElimination Error :universeIsType,  sqequalBase Error :equalityIstype,  voidElimination equalitySymmetry equalityTransitivity independent_isectElimination intEquality cumulativity instantiate Error :productIsType,  Error :setIsType,  Error :lambdaFormation_alt,  lambdaFormation dependent_set_memberEquality dependent_set_memberFormation addEquality because_Cache rename setElimination multiplyEquality productEquality lambdaEquality independent_functionElimination isectElimination hypothesis baseClosed hypothesisEquality imageMemberEquality independent_pairFormation sqequalRule natural_numberEquality Error :dependent_set_memberEquality_alt,  thin dependent_functionElimination sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution sqequalHypSubstitution extract_by_obid introduction cut

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



Date html generated: 2019_06_20-PM-02_35_15
Last ObjectModification: 2019_06_12-PM-00_56_24

Theory : num_thy_1


Home Index